\subsection{Syntax}
The syntax of networking in Casanova is rather simple. In the following we only provide an intuitive illustration of the terms that can be used, and a first description of their purpose.

The first series of supported keywords are those that are used for determining ownership of entities. The keywords below are all used to delimit the \textit{scope} within which a given set of rules is valid:

\begin{lstlisting}
local { ... }
remote { ... }
\end{lstlisting}

Every entity in Casanova is duplicated across all the current instances of the game. Only one of this instances has ownership of the entity, that is acts as the authoritative instance which updates the entity for all other instances. The rules that perform such updates, and which also send the updates to the other instances, are all defined inside a \texttt{local} block. The rules that are executed in all the other, remote, instances are all defined inside a \texttt{remote} block.

Another keyword, which is used nested in \texttt{local} or \texttt{remote}, is:

\begin{lstlisting}
connect { ... }
\end{lstlisting}

When a new instance of the game connects, then we also run, just once, all the rules inside the \texttt{connect} block. When a new instance is run, then its \texttt{local connect} rules are run once. When existing instances, on the other hand, witness the start of a new instance, then their \texttt{remote connect} rules are run once.

There are only four primitives for transmitting data across the network. Two are for sending data, and two are for receiving. Sending simply takes as input a value of any type, and returns nothing. Sending may also be done reliably, thereby trying to ensure that the other party has indeed received the message. Reliable sending may fail, for example if the receiver disconnects during the transmission. For this reason, sending reliably returns a boolean value that will be \texttt{true} if the transmission was successful, and \texttt{false} if the transmission failed for some reason:

\begin{lstlisting}
send<T> : T -> Unit
send_reliable<T> -> bool
\end{lstlisting}

As a convenience, it is possible to, at the same time, locally store a value and send it across the network. For this purpose, we can use the \texttt{+send} syntax, which both \textit{sends and returns} the expression that is passed as an argument to \texttt{+send}:

\begin{lstlisting}
yield +send<T>(x)
\end{lstlisting}

Receiving may also be done in two different manners. Simple reception of a message is done with the \texttt{receive} primitive that returns a value of some type \texttt{T}. Receiving may also be done by all other instances at the same time, for example when voting or for other kinds of global synchronization. In this case, we wait until all other instances have each sent their value of some type \texttt{T}, and then we return all said values in a list of \texttt{T}s:

\begin{lstlisting}
receive<T> : Unit -> T
receive_many<T> : Unit -> List<T>
\end{lstlisting}

\subsection{Semantics}
In the following we discuss the semantics of Casanova networking, but not in formal terms. Rather, we suggest a translation from Casanova with networking into Casanova without networking, assuming that one of the external libraries that Casanova is using is providing some low-level networking service.

Networking in Casanova is based on two separate systems. The first such system is the underlying networking library that is accessed as an external service to be orchestrated. This is directly \textit{linked} to all programs that need networking functionalities. Multiple versions of this service may exist for different networking libraries, but in general we can assume that not many such services need to be built, and that there is a one-to-many relationship between networking services and actual games. The second system is the Casanova compiler itself, which modifies entity declarations and even defines whole new entities. The compiler will, effectively, translate away all networking operations and keywords (even \texttt{local}, \texttt{remote}, and \texttt{connect}) and turn them into much simpler operations on lists. The only assumption made that really has anything to do with networking is that some special memory locations are actually written to or read from the network.

\subsubsection{Common primitives}
We now present the common primitives that are provided by the networking service. The core of the networking service is the \texttt{NetManager}. The \texttt{NetManager} maintains the connections between the local instance of the game and the remote instances:

\begin{lstlisting}
entity NetManager = {
\end{lstlisting}

The \texttt{NetManager} maintains a list of \texttt{NetPeer}s. Each \texttt{NetPeer} represents a remote instance of the game. The \texttt{NetManager} also store the unique \texttt{Id} associated with the local instance:

\begin{lstlisting}
  Peers         : List<NetPeer>
  Id            : PeerId
\end{lstlisting}

The \texttt{NetManager} also manages two flags, which will be used to determine when the \texttt{local connect} and the \texttt{remote connect} rules are run:

\begin{lstlisting}
  localConnect : bool
  remoteConnect  : bool
\end{lstlisting}

The \texttt{localConnect} flag may run only once, at the beginning of the game. The game world will then reset the flag to \texttt{false} when the \texttt{local connect} rules are all terminated.

Whenever a new connection is established with a new \texttt{NetPeer}, then we add that peer to the list of \texttt{Peers}, and we set \texttt{remoteConnect} to \texttt{true} so that the local \texttt{remote connect} rules may be run. Notice that we wait for \texttt{remoteConnect} to be set to false, which is only done by the game world when the current \texttt{remote connect} rules all terminate. This allows us to process all new connections one at a time:

\begin{lstlisting}
  rule Peers, remoteConnect =
    wait_until(remoteConnect = false)
    let new_peer = wait_some(NetPeer.NewPeer())
    yield Peers + new_peer, true
\end{lstlisting}

Every few seconds, we check which peers disconnected and remove them from the list of peers. The disconnection is all managed internally by the underlying networking library:

\begin{lstlisting}
  rule Peers = 
    wait 5.0f<s>
    from p in Peers
    where p.Channel.Connected
    select p
\end{lstlisting}

We initialize the \texttt{NetManager} by finding all reachable peers across the network. We use their current \texttt{Id} values to find an \texttt{Id} for this instance that is unique to this game session. We also set \texttt{localConnect} to true, since we need to send the locally managed values to the other instances, and \texttt{remoteConnect} to false:

\begin{lstlisting}
  Create() =
    let peers = NetChannel.FindPeers()
    {
      Id            = from p in peers
                      max_by p.Id + 1
      Peers         = peers
      localConnect = true
      remoteConnect  = false
    }
}
\end{lstlisting}

Another, remote instance of the game is represented by the \texttt{NetPeer}. A \texttt{NetPeer} is responsible for handling the actual communication to the other instances of the game:

\begin{lstlisting}
entity NetPeer = {
\end{lstlisting}

The \texttt{NetPeer} contains a channel, which is an instance of a data-type supplied by some network library and which will, automatically, send and receive messages. The \texttt{NetPeer} also contains an \texttt{Id} which uniquely identifies it among the various instances of the game, and a list of messages received so far:

\begin{lstlisting}
  Channel           : NetChannel
  Id                : PeerId
  ReceivedMessages  : List<InMessage>
\end{lstlisting}

The list of messages received so far is constantly refreshed with the list of received messages automatically populated by the channel:

\begin{lstlisting}
  rule ReceivedMessages = yield Channel.ReceivedMessages
\end{lstlisting}

The \texttt{NetPeer} also looks for all the messages that need to be sent across the game world, both reliably and unreliably. These messages are then written into the \texttt{SentMessages} and \texttt{ReliablySentMessages} lists of the underlying channel: 

\begin{lstlisting}
  rule Channel.SentMessages = 
    from (m:OutMessage) in *
    where exists(Id, m.Targets) || m.Targets = []
    select m
  rule Channel.ReliablySentMessages = 
    from (m:ReliableOutMessage) in *
    where exists(Id, m.Targets) || m.Targets = []
    select m
}
\end{lstlisting}

The underlying networking library is also expected to provide a series of data types which represent messages and channels. We do not care about the concrete shape of the data types, as long as they contain the required properties.

The simple message only needs to handle the \textit{Casanova header}, which stores which instance of the game sent this message, what type of data the message contains, and the entity from which this message was sent:

\begin{lstlisting}
interface Message
  Sender          : PeerId
  ContentType     : TypeId
  OwnerEntity     : EntityId
\end{lstlisting}

An outgoing message inherits from \texttt{Message}. It also has a list of target instances to which this message is addressed. The list of targets may also be empty, in which case we wish to send the message to all reachable peers. An \texttt{OutMessage} also offers a series of low-level write methods to send various primitive values such as integers, floating-point numbers, strings, etc.:

\begin{lstlisting}
interface OutMessage
  inherit Message
  Targets             : List<PeerId>
  member WriteInt     : int -> Unit
  member WriteFloat   : float32 -> Unit
  member WriteString  : string -> Unit
  member WriteT       : T -> Unit // only for elementary data-types
\end{lstlisting}

Almost identical to the \texttt{OutMessage} is the \texttt{ReliableOutMessage}. A reliable outgoing message only differs from a simple outgoing message in that it also has properties that tells us whether or not the message has been received or the transmission has failed:

\begin{lstlisting}
interface ReliableOutMessage
  inherit Message
  Targets             : List<PeerId>
  member WriteInt     : int -> Unit
  member WriteFloat   : float32 -> Unit
  member WriteString  : string -> Unit
  ...
  member Received     : bool
  member Failed       : bool
\end{lstlisting}

A received message inherits from the simple \texttt{Message}, and also offers a series of low-level write methods to read various primitive values such as integers, floating-point numbers, strings, etc.:

\begin{lstlisting}
interface InMessage
  inherit Message
  member ReadInt     : Unit -> int
  member ReadFloat   : Unit -> float32
  member ReadString  : Unit -> string
  ...
\end{lstlisting}

The final data-type that is provided by the networking library is the communication channel itself. Casanova requires a channel to expose the messages which were just received, and lists where the messages to be sent can be put. Also, the channel should provide a (static) mechanism to find those peers that just connected:

\begin{lstlisting}
 interface NetChannel
  member ReceivedMessages       : List<InMessage>
  member SentMessages           : List<OutMessage>
  member ReliablySentMessages   : List<ReliableOutMessage>
  static member FindPeers       : Unit -> List<NetPeer>
\end{lstlisting}

Notice that in the listings above we have slightly abused the notion of \textit{interface}. We have used a notion that resembles more closely that of a \textit{type-trait} or a \textit{type-class}, but the abuse is quite minor and we believe the idea of an interface to capture the essence of what Casanova expects from the underlying library.

\subsubsection{Chat sample translated}
Inside an application, the compiler generates a series of additional entities and modifies the game rules in order to accommodate networking primitives. The generated entities are all wrappers for messages, both incoming and outgoing. A pair of incoming/outgoing message entities is created for each type \texttt{T} such that a \texttt{send<T>} and a \texttt{receive<T>} appear in the game rules. In the case of the chat sample, we only ever send strings, so only one such pair is generated.

One generated entity inherits from \texttt{InMessage} and contains a string value which was just received:

\begin{lstlisting}
entity InMessageString = {
  inherit InMessage
  Value : string
\end{lstlisting}

When creating an \texttt{InMessageString}, we take a simpler \texttt{InMessage}, ``parse''\footnote{\textit{Parsing} in this context is a bit of an excess.} it by invoking \texttt{ReadString} once, and then store message and string:

\begin{lstlisting}
  Create(msg : InMessage) =
    let value = msg.ReadString()
    {
      InMessage = msg
      Value     = value
    }
}
\end{lstlisting}

The dual of the entity we have just seen is the \texttt{ReliableOutMessageString}, which inherits from the simpler \texttt{ReliableOutMessage}:

\begin{lstlisting}
entity ReliableOutMessageString = {
  inherit ReliableOutMessage
\end{lstlisting}

When we create a \texttt{ReliableOutMessageString}, in reality we create a \texttt{ReliableOutMessage} and write the content of the message (a string) to it with \texttt{WriteString}:

\begin{lstlisting}
  Create(value : string, targets : List<Peer>, sender : ConnectionId, owner_entity : EntityId) =
    let m = new ReliableOutMessage(sender, StringTypeId, owner_entity, targets)
    do m.WriteString(m)
    {
      ReliableOutMessage = m
    }
}
\end{lstlisting}

At this point we can move on to the definition of the game world. The first two fields are identical to the sample as we have seen it in previously. Local rules that do not \texttt{send} or \texttt{receive} are unchanged:

\begin{lstlisting}
world Chat = {
  Text                  : string
  Line                  : string
  
  ...
\end{lstlisting}

The compiler also adds a series of additional fields. One of the fields is a network manager, which will manage the various connections. Two lists, one for incoming and one for outgoing messages are also declared. Finally, an \texttt{Id} is used to store a unique identifier for this specific entity:

\begin{lstlisting}
  Network               : NetManager
  Inbox                 : List<InMessageString>
  Outbox                : List<ReliableOutMessage>
  Id                    : EntityId
\end{lstlisting}

We automatically empty the list of outgoing messages, in the assumption that the \texttt{NetPeer} instances have already stored them and are handling them:

\begin{lstlisting}
  rule Outbox = yield []
\end{lstlisting}

We fill the list of incoming messages from the incoming messages found in the channels of the various peers. We filter those messages, so that only those that were specifically aimed towards this entity (and contain data of the expected type, in our case \texttt{string}) are kept:

\begin{lstlisting}
    yield Inbox +
          from c in Network.Peers
          from m in c.ReceivedMessages
          where m.ContentType = StringTypeId &&
                m.OwnerEntity = Id
          select InMessageString.Create(m.Value)
\end{lstlisting}

When we want to send a string, we also create a message with the string we wish to send, add it to the \texttt{Outbox} list, and wait until the message is received. The rest of the rule is unchanged:

\begin{lstlisting}
  rule Line, Text, Outbox = 
    wait_until(IsKeyDown(Keys.Enter))
    let msg = ReliableOutMessageString.Create(Line, [], Network.Id, Chat.TypeId, Id).ReliableOutMessage
    yield Outbox <- Outbox + msg
    wait_until(msg.Received)
    yield Line <- "", Text <- Text + "\n" + Line
\end{lstlisting}

Essentially, \texttt{send\_reliably<string>} turns into the following lines:

\begin{lstlisting}
    let msg = ReliableOutMessageString.Create(Line, [], Network.Id, Id).ReliableOutMessage
    yield Outbox <- Outbox + msg
    wait_until(msg.Received)
\end{lstlisting}

In particular, we create the output message by also specifying:
\begin{itemize}
\item the message recipients, which are the empty list \texttt{[]} which means that the message will be sent to all other peers
\item the peer that is the sender (and owner) of the message, which is \texttt{Network.Id}
\item the entity that the message was sent from, which is simply the world \texttt{Id}
\end{itemize}

We consider a message received when it appears in the \texttt{Inbox} list. When we find one, we remove it from the list, and process it as the result of the \texttt{receive} function:

\begin{lstlisting}
  rule Text, Inbox =
    wait_until (Inbox.Length > 1)
    yield Text + "\n" + Inbox.Head.Value, Inbox.Tail
\end{lstlisting}

Essentially, \texttt{receive<string>} has turned into:

\begin{lstlisting}
    wait_until (Inbox.Length > 1)
    Inbox.Head.Value // the received string
\end{lstlisting}

The creation of the world now simply initializes the network manager, creates a new unique id for the entity, and then initializes the various other fields with empty values:

\begin{lstlisting}
  Create() =
    let network = NetManager.Create()
    let id = NetManager.NextId()
    {
      Text                  = ""
      Line                  = ""
      Id                    = id
      Network               = network
      Inbox                 = []
      Outbox                = []
      StringsInbox          = []
    }
}
\end{lstlisting}

As we can see from the sample, it is possible to translate away the networking primitives, provided a very small component capable of sending and receiving messages created from an aggregation of elementary data structures.

\subsubsection{Lobby sample translated}
In this more complete example we also see how local and remote blocks are handled, both at connection time and during the main run.

The lobby sample generates four entities for (reliably) sending and receiving \texttt{bool} and \texttt{LobbyPlayer} values. The \texttt{bool} message entities are almost identical to the \texttt{string} ones that we have seen in the chat sample, and so we omit them. The \texttt{LobbyPlayer} message entities, on the other hand, are more articulated. A received \texttt{LobbyPlayer} will have an underlying incoming message and the \texttt{LobbyPlayer} itself:

\begin{lstlisting}
entity InMessageLobbyPlayer = {
  inherit InMessage
  Value : LobbyPlayer
\end{lstlisting}

When we create the \texttt{InMessageLobbyPlayer}, we parse its contents. First we read the player \texttt{name}, then its \texttt{ready} status, and then the \texttt{X} and \texttt{Y} of its starting position. The \texttt{id} of the player is stored in the underlying message, so we do not need to read it again and can reuse it directly. Finally, the owner of the entity is its sender, and the received entity will thus be remoted to the underlying message sender:

\begin{lstlisting}
  Create(msg : InMessage) =
    let name        = msg.ReadString()
    let ready       = msg.ReadBool()
    let start_pos   = Vector2(msg.ReadFloat(), msg.ReadFloat())
    let id          = msg.EntityId
    let ownership   = remote(msg.Sender)
    {
      InMessage = msg
      Value =
        {
          Name           = name
          Ready          = ready
          StartPosition  = start_pos
          Id             = id
          InboxBool      = []
          Outbox         = []
          Ownership      = ownership
        }
    }
}
\end{lstlisting}

Similarly, we define the \texttt{ReliableOutMessageLobbyPlayer} as a wrapper over the simpler \texttt{ReliableOutMessage}:

\begin{lstlisting}
entity ReliableOutMessageLobbyPlayer = {
  inherit ReliableOutMessage
\end{lstlisting}

When we send a \texttt{LobbyPlayer} we first create the underlying message with the Casanova header of sender, owner entity, etc. Then, we perform a series of \texttt{write} operations that mirror the \texttt{read} operations in the \texttt{InMessageLobbyPlayer}:

\begin{lstlisting}
  Create(value : LobbyPlayer, targets : List<Peer>, sender : ConnectionId, owner_entity : EntityId) =
    let m = new ReliableOutMessage(sender, LobbyPlayerTypeId, owner_entity, targets)
    do m.WriteString(value.Name)
    do m.WriteBool(value.Ready)
    do m.WriteFloat(value.StartPosition.X)
    do m.WriteFloat(value.StartPosition.Y)
    {
      ReliableOutMessage = m
    }
}
\end{lstlisting}

The \texttt{Lobby} itself contains the same fields that store the various players:

\begin{lstlisting}
world Lobby = {
  Self                  : LobbyPlayer
  Others                : List<LobbyPlayer>
\end{lstlisting}

Additionally, the compiler generates a series of networking-related fields. The entity has a networking manager, and \texttt{id}, and a series of lists for storing incoming and outgoing messages. In particular, it may seem as we receive \texttt{LobbyPlayers} twice, but we actually store the received lobby players for both \texttt{receive} and \texttt{receive\_many}:

\begin{lstlisting}
  Network               : NetManager
  Id                    : int
  InboxLobbyPlayer      : List<InMessageLobbyPlayer>
  InboxListLobbyPlayer  : List<InMessageLobbyPlayer>
  Outbox                : List<ReliableOutMessage>
\end{lstlisting}

Just like we did for the chat, we empty the list of outgoing messages, and fill in the lists of \texttt{LobbyPlayer} messages from the various peers:

\begin{lstlisting}
  rule Outbox = yield []
  rule InboxListLobbyPlayer = 
    yield InboxListLobbyPlayer +
          from c in Network.Peers
          from m in c.ReceivedMessages
          where m.ContentType = LobbyPlayerTypeId &&
                m.OwnerEntity = Id
          select InMessageLobbyPlayer.Create(m.Value)
  rule InboxLobbyPlayer = 
    yield InboxLobbyPlayer +
          from c in Network.Peers
          from m in c.ReceivedMessages
          where m.ContentType = LobbyPlayerTypeIdTypeId &&
                m.OwnerEntity = Id
          select InMessageLobbyPlayer.Create(m.Value)
\end{lstlisting}

The \texttt{local connect} waits until the network manager sets its \texttt{localConnect} flag to \texttt{true}. This will only allow the rule to run once upon first connection, and then stop:

\begin{lstlisting}
  rule Self, Others, InboxListLobbyPlayer, Outbox, Network.localConnect =
    wait_until(Network.localConnect = true)
\end{lstlisting}

We now perform a \texttt{receive\_many} by waiting until all peers have sent us something. We then take one received \texttt{LobbyPlayer} per peer:

\begin{lstlisting}
    wait_until(from m in InboxListLobbyPlayer
               select m
               group_by m.Sender
               count = Network.Peers.Length)
    let others = // take one item per peer
      from m in InboxListLobbyPlayer
      select m
      group_by m.Sender as g
      select g.Elements.Head.Value
    yield InboxListLobbyPlayer <- []
\end{lstlisting}

We then send our own \texttt{LobbyPlayer}, and wait until it has been received by all:

\begin{lstlisting}
    let max_x = 
      maxby p in others
      select p.StartPosition.X
    let start_position = Vector2(max_x + 5.0f<pixel>, 0.0f<pixel>)
    let self = { Self with Position = start_position }
    let msg = ReliableOutMessageLobbyPlayer.Create(Self, [], Network.Id, Id).ReliableOutMessage
    yield Outbox <- Outbox + msg
    wait_until(msg.Received)
\end{lstlisting}

Finally, we store the players locally, and reset \texttt{localConnect} to \texttt{false}. A very important notice is that, in case of multiple \texttt{local connect} rules, then we need to wait until all of them are done before resetting \texttt{localConnect}. This will require additional boolean flags:

\begin{lstlisting}
    yield Self <- self, Others <- others, Network.localConnect <- false
\end{lstlisting}

The \texttt{remote connect} waits until the network manager sets its \texttt{remoteConnect} flag to \texttt{true}. This will only allow the rule to run once for every new connection, and then stop:

\begin{lstlisting}
  rule Others, InboxLobbyPlayer, Outbox, Network.remoteConnect =
    wait_until(Network.remoteConnect = true)
\end{lstlisting}

We send the local player to the new instance, and wait for the message to be received:

\begin{lstlisting}
    let msg = ReliableOutMessageLobbyPlayer.Create(Self, [], Network.Id, Id).ReliableOutMessage
    yield Outbox <- Outbox + msg
    wait_until(msg.Received)
\end{lstlisting}

We then received the local player of the new instance:

\begin{lstlisting}
    let new_player = receive<LobbyPlayer>()
    wait_until(InboxLobbyPlayer.Length > 1)
    let others = InboxLobbyPlayer.Head.Value
    yield InboxLobbyPlayer <- InboxLobbyPlayer.Tail
\end{lstlisting}

Finally, we add the new player to the list of players, and reset \texttt{remoteConnect} to \texttt{false}. A very important notice is that, in case of multiple \texttt{remote connect} rules, then we need to wait until all of them are done before resetting \texttt{remoteConnect}. This will require additional boolean flags:

\begin{lstlisting}
    yield Others <- Others + new_player, Network.remoteConnect <- false
\end{lstlisting}

Starting the game waits for all players to be ready. This rule is unchanged:

\begin{lstlisting}
  rule CurrentWorld = 
    wait_until(Self.Ready &&
               from p in Others
               select p.Ready)
    yield Arena.Create(Self)
\end{lstlisting}

We create the game like we did for the chat sample. We initialize the network and local fields, and start the various inbox and outbox lists to empty lists:

\begin{lstlisting}
  Create(own_name) = 
    let network = NetManager.Create()
    let id = network.NextId
    {
      Self                  = LobbyPlayer.Create(own_name, Vector2.Zero, network)
      Others                = []
      Network               = network
      Id                    = id
      InboxLobbyPlayer      = []
      InboxListLobbyPlayer  = []
      Outbox                = []
    }
}
\end{lstlisting}

We can now present the \texttt{LobbyPlayer} itself. The entity contains its original fields of name, readiness, and initial position for the game:

\begin{lstlisting}
entity LobbyPlayer = {
  Name                  : string
  Ready                 : bool
  StartPosition         : Vector2<pixel>
\end{lstlisting}

The entity also has a network \texttt{id}, plus an \texttt{ownership} value that indicates whether or not the entity is owned by the local instance (in which case \texttt{Ownership = local}) or whether it is owned by a remote peer (in which case \texttt{Ownership = remote(Peer)} where \texttt{Peer} is the \texttt{Id} of the owner). The entity also contains a list of received and unprocessed \texttt{bool} messages, and a list of outgoing messages that will be sent:

\begin{lstlisting}
  Id                    : int
  Ownership             : NetOwnership
  InboxBool             : List<InMessageBool>
  Outbox                : List<ReliableOutMessage>
\end{lstlisting}

We automatically empty the list of outgoing messages, in the assumption that the \texttt{NetPeer} instances have already stored them and are handling them, and we store locally the received messages of type \texttt{bool} and destined to this entity:

\begin{lstlisting}
  rule Outbox = yield []
  rule InboxBool = 
    yield InboxBool +
          from c in Network.Peers
          from m in c.ReceivedMessages
          where m.ContentType = BoolTypeId &&
                m.OwnerEntity = Id
          select InMessageBool.Create(m.Value)
\end{lstlisting}

The local rules all run exclusively if the entity is locally owned. For this reason we wait, just once, that \texttt{Ownership = local}, and then we loop forever the body of the rule because ownership does not change:

\begin{lstlisting}
  rule Ready, Outbox = 
    wait_until(Ownership = local)
    while(true)
\end{lstlisting}

Whenever the \texttt{Enter} key is pressed, we create a reliable outgoing boolean message and then put it in the outgoing queue of messages. We then wait until the message is received:

\begin{lstlisting}
      wait_until(IsKeyDown(Enter))
      let msg = ReliableOutMessageBool.Create(true, [], world.Network.Id, Id).ReliableOutMessage
      yield Outbox <- Outbox + msg
      wait_until(msg.Received)
\end{lstlisting}

Finally, we set the local value of \texttt{Ready} to \texttt{true}:

\begin{lstlisting}
      yield Ready <- true
\end{lstlisting}

The remote rules all run exclusively if the entity is remotely owned. For this reason we wait, just once, that \texttt{Ownership <> local}, and then we loop forever the body of the rule because ownership does not change:

\begin{lstlisting}
  rule Ready, InboxBool = 
    wait_until(Ownership <> local)
    while(true)
\end{lstlisting}

We wait until a boolean message appears in the incoming queue. We then return this message, and discard it from the queue as it has now been processed:

\begin{lstlisting}
      wait_until(InboxBool.Length > 1)
      yield InboxBool.Head.Value, InboxBool.Tail
\end{lstlisting}

We create the entity from its original parameters, but we also need the local \texttt{NetManager} in order to obtain a unique \texttt{Id} for the entity. We also initialize the various message lists to empty lists. Finally, when creating an entity locally we will always set its \texttt{Ownership} to \texttt{local}, because the entity is owned by the peer that creates it:

\begin{lstlisting}
  Create(name, p, network : NetManager) = 
    {
      Name          = name
      Ready         = false
      StartPosition = p
      Id            = network.NextId
      InboxBool     = []
      Outbox        = []
      Ownership     = local
    }
}
\end{lstlisting}


\subsection{Formal semantics}
We now present the semantics in a more formal and compact framework. To describe the way multi-player games work, we consider the various instances of the game running in lock-step. Each instance has its own game world:

$$\omega_1, \omega_2, \dots$$

The game world is structured like a tree of entities. Each entity has some fields and some rules. Each rule acts on a subset of the fields of the entity by defining their new value after one (or more) ticks of the simulation. For simplicity, in the following we assume that each rule updates all fields together\footnote{\texttt{rule X = yield 10} is equivalent to \texttt{rule X,Y,Z = yield 10,Y,Z}}:

$$E = { f_1 \dots f_n \ \ r_1 \dots r_m }$$

An entity is updated by evaluating, in order, all the rules to the fields:

\begin{align*}
\tick(e:E, dt) = { \tick(f_1',dt) \dots \tick(f_n',dt) \ \ r_1' \dots r_m' }\\
f_1',\dots,f_n',r_1',\dots,r_m' = \step(\dots \step(f_1,\dots,f_n,r_1), \dots, r_m)
\end{align*}

We define the $\step$ function as a function that recursively evaluates the body of a rule. The function evaluates until it encounters either a $\wait$ or a $\yield$ statement. $\step$ also returns the remainder of the rule body, so that the rule will effectively be resumed where it left off, at the next evaluation of $\step$:

\begin{align*}
\step(f_1, \dots, f_n, \letlet x = y \letin z) = \step(f_1, \dots, f_n, z[x:=y]) \\
\vdots \\
\step(f_1, \dots, f_n, \yield x; b) = x, b
\end{align*}

In order to add networking, we assume that each entity has two new fields, which are $\id$ and $\owner$. $\id$ is a simple (numeric) identifier that, inside a single instance of the game world, uniquely denotes a specific entity. $\owner$ may be either $\local$ or $\remote$. Given a set of entities (one per game world) that share the same type and the same $\id$, exactly one of them will be $\local$, all the others will be $\remote$.

First of all we ``translate away'' the $\local$ and $\remote$ scopes. This means that given an entity with some rules defined inside such scopes:

$$E = { f_1 \dots f_n \ \ r_1 \dots \ \ \local{ r_j \dots } \remote{ r_l \dots } }$$

we transform the rules $r_j$ inside the $\local$ scope into:

$$\wait(\owner = \local); r_j$$

and we transform the rules $r_j$ inside the $\remote$ scope into:

$$\wait(\owner = \remote); r_l$$

This will prevent those rules from running when they should not. Similarly, by adding the global $\localconnect$ and $\remoteconnect$ flags, we can have some rules only execute when a new instance is added to the game. All existing instances will enable $\remoteconnect$, while the new instance will enable $\localconnect$.

When evaluating a rule with the $\step$ function, we stop at $\receive[T]$ statements. Assume that we are updating entities inside a specific game instance, the one with the world $\omega_i$. We look for some entity, $e'$, belonging to \textit{another} game world, with the same $\id$ as the entity we are updating, and which is sending a value $v$ of the type we are expecting ($T$):

$$\step(f_1, \dots, \letlet x = \receive[T](); b) =
\left\{
\begin{matrix}
f_1, \dots, b[x:=v'] \ \ \text{when } \exists r_l \in e' : r_l = \send[T](v) \\
f_1, \dots, \letlet x = \receive[T](); b \ \ \text{otherwise}
\end{matrix}
\right.
$$

Notice that when we receive a value $v$, we turn it into $v'$ in the receiving instance of the game. $v'$ is identical to $v$, but all of its $\owner$ fields are changed to $\remote$. This is needed in order to reflect the fact that even if the transmitted entity was owned by the sender, it is certainly not owned by the receiver. Similarly, when performing a $\receiveMany$, then we look for another entity $e'_j$ with the same type and $\id$ of the current entity \textit{for each other game world}:

$$\step(f_1, \dots, \letlet x = \receiveMany[T](); b) =
\left\{
\begin{matrix}
f_1, \dots, b[x:=[v'_1 \dots ]] \ \ \text{when } \forall e'_j : \exists r^j_l \in e'_j : r^j_l = \send[T](v^j) \\
f_1, \dots, \letlet x = \receiveMany[T](); b \ \ \text{otherwise}
\end{matrix}
\right.
$$

$\receiveMany$ then binds the list of \textit{all the received values} to $x$. Both $\receive$ and $\receiveMany$ also work with $\sendRel$, and not just with $\send$. The main difference is that $\send$ does not wait to be evaluated, while $\sendRel$ waits until someone performs a $\receive$ or a $\receiveMany$. Thus, $\send$ is eagerly stepped:

$$\step(f_1, \dots, \send[T](v); b) = f_1, \dots, b$$

while $\sendRel$ needs to wait:

$$\step(f_1, \dots, \sendRel[T](v); b) =
\left\{
\begin{matrix}
f_1, \dots, b \ \ \text{when } \exists r_l \in e' : r_l = \receive[T]() \\
f_1, \dots, \sendRel[T](v); b \ \ \text{otherwise}
\end{matrix}
\right.
$$

The semantics of sending and receiving are thus easily explained in terms of changes to the values (and the control flow) of other instances, with some added machinery to make sure that only the appropriate rules (\texttt{local}, \texttt{remote}, etc.) are run on each instance.

\subsection{Reliability}
One aspect that has not been covered so far is handling of transmission failures. All primitives but $\sendRel$ never fail. $\sendRel$, on the other hand, may fail when the receiver is either disconnected or unreachable. After a certain time-out, $\sendRel$ will return \texttt{false} to denote transmission failure, and inform the other instances that the receiver should be considered disconnected. This means that $\sendRel$ are implicitly used for forcing disconnection of unreachable instances.

\subsection{Asymmetry and load sharing}
The ability to determine which instance of the game runs which entities locally allows us to take advantage of asymmetry for performance purposes. By estimating the network and CPU performance of an instance, we can determine its current overall performance. Overall performance of an instance could be used to have that instance create, and handle, more performance-intensive entities, such as those with complex AI, physics, etc. This way instances that have more processing power (for example because of better hardware) or bandwidth (because of a better local network infrastructure) would be used to lighten the load of the ``weaker'' instances.

This topic is quite broad and complex, and it is outside the scope of the current work. For this reason we do not expand it in depth, but leave it sketched.

\subsection{Closing remarks}
This concludes the presentation of Casanova syntax and semantics. The syntax may look, at a first glance, deceptively simple, but in reality it drives a complex translation. All networking operations are then translated away in a series of list operations on incoming or outgoing mailboxes. The various mailboxes then handle messages, which are responsible for the low-level sending and receiving of data through some simple, low-level, underlying networking library that is required to provide little more than sockets and connections.
