\documentclass[11pt]{article}
\newcommand{\tuple}[1]{\ensuremath \langle #1 \rangle}
\usepackage{color}
\usepackage{amsthm}
\usepackage{amsmath}
\usepackage{graphicx}
\usepackage{mathrsfs}
\usepackage{amssymb}
\usepackage{algpseudocode}% http://ctan.org/pkg/algorithmicx
\usepackage[all]{xy}
\usepackage{varwidth}

\newtheorem{theorem}{Theorem}
\newtheorem{prop}{Proposition}
\newtheorem{lem}{Lemma}
\newtheorem{defn}{Definition}
\newcommand{\note}[1]{{\color{red} \bf [[#1]]}}
\newcommand{\push}[1][1]{\hskip\dimexpr #1\algorithmicindent\relax}
\newcommand*\xor{\mathbin{\oplus}}
\begin{document}


\setlength\parindent{0pt} % Removes all indentation from paragraphs - comment this line for an assignment with lots of text


\section{\textbf{Introduction}}







\section{\textbf{Server}}
The server maintains a collection of slots such that each slot contains some data.
The operations on the slot are as follows:
\begin{itemize}
    \item Put slot
    \item Get slot
    \item Delete Slot
\end{itemize}

\subsection{\textbf{Server Notation Conventions}}
$s \in SN$ is a server sequence number\\
$sv \in SV$ is a slot's value\\
$slot_s = \tuple{s, sv} \in SL \subseteq SN \times SV$

\subsection{\textbf{Server State}}
\textit{n = current server sequence number}\\
\textit{SL = set of live slots on the server}\\

\textbf{Initial Server State}\\
$SL = \emptyset$\\
$n = 0$

\subsection{\textbf{Put Slot}}
Put slot is an operation that inserts data into a new slot at the server.\\

%Put Function
\noindent\fbox{%
\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}
\textbf{Put Function:}
\begin{algorithmic}[1]
\Function{PutSlotServer}{$sv_p$}
    \State $s_p \gets n$
    \State $n \gets n + 1$
    \State $SL \gets SL \cup \{\tuple{s_p,sv_p}\}$
\EndFunction
\end{algorithmic}
\end{varwidth}% 
}

\subsection{\textbf{Get Slot}}
Get slot is an operation that returns all server slots that are greater than some server sequence number.\\

% Get Function
\noindent\fbox{%
\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}
\textbf{Get Function:}
\begin{algorithmic}[1]
\Function{GetSlotServer}{$s_g$}
    \State \Return{$\{\tuple{s, sv} \in SL \mid s \geq s_g\}$}
\EndFunction
\end{algorithmic}
\end{varwidth}% 
}

\subsection{\textbf{Delete Slot}}
Delete slot is an operation that deletes all live slots that have server sequence numbers that are equal to or less than some server sequence number.\\

%Delete Function
\noindent\fbox{%
\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}
\textbf{Delete Function:}
\begin{algorithmic}[1]
\Function{DeleteSlotServer}{$s_d$}
    \State $SD \gets \{\tuple{s, sv} \in SL \mid s \leq s_g\}$
    \State $SL \gets SL - SD$
\EndFunction
\end{algorithmic}
\end{varwidth}% 
}








\section{\textbf{Client}}
The data structure acts as a key store where key-value pairs can be read and set.
The data structure exposes the following functions:
\begin{itemize}
    \item Put Transaction
    \item Get key-value pair
    \item Create new key
\end{itemize}

\subsection{\textbf{Client Notation Conventions}}

$K$ is the set of all keys.\\
$MID$ is the set of the machine IDs of the devices that are in the system.
$K_{mid}$ is a set of all keys that have device mid as the arbitrator\\
$ssn_s$ is the server sequence number of a record $s$\\
$mid_s \in MID$ is the machine ID for the device that created $record_s$.\\
$hmac_s$ is the HMAC of $record_s$\\
$c_{mid}$ is the latest read clock for a device with machine ID $mid$\\
$vc_s = \{c_{mid} | mid \in MID\}$\\
$rid_s = \tuple{mid_s, c_{mid_s}}$
$k$ is a key entry\\
$v$ is a value entry\\
$kv_n$ is a key-value entry $\tuple{k_n,v_n} , k \in K$\\

$tid_s = \tuple{mid_s,c_{mid_s}}$\\
$guard_s = \tuple{\{kv_1, kv_2, ... ,kv_n | \exists mid \in MID, \forall n, kv_n[k] \in K_{mid}\},$ boolean condition using $ \{kv_1, kv_2, ... ,kv_n\}} $\\
$transaction_s = \{mid_s,vc_{s_t} ,\{kv_1, kv_2,...kv_n | \exists mid \in MID, mid = guard_s[mid], \forall n, kv_n[k] \in K_{mid}\},guard_s\}$\\
$commit_s = \tuple{tid_s,vc_s}$\\
$abort_s = \tuple{tid_s,mid_s,vc_s}$\\
$sequence_s = \tuple{rid_s, ssn_s}$\\
$delete_s = \tuple{ssn_d}$\\
$resize_s = \tuple{x | x \in \mathbb{N}}$\\
$newkey_s = \tuple{k_s, vc_s, ssn_s$ or $-1, mid_s}$\\

$payload_s = \{x_1, x_2,..., x_k | \forall k, x_k \in \{$transaction, commit, abort, resize, newkey, sequence, delete$\}\}$\\
$rd_s = \tuple{mid_s, vc_s, hmac_s, payload_s}$ \\
$record_s = \tuple{ssn_s,rd_s}$\\

\subsection{\textbf{Client State}}
\textit{s = largest server sequence number pulled from the server by a device} \\
\textit{R = set of records pulled from the server so far with their server sequence numbers} \\
\textit{RL = set of records that contain live data} \\

\subsection{Helper Functions}
The following helper functions are needed:\\

%Get Payload Items from Record with SSN
\noindent\fbox{%
\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}
\textbf{Get Payload Items from Record with SSN}:
\begin{algorithmic}[1]
\Function{GetPayloadItemsWithSSN}{$record_s$}
    \State $PISSN \gets \emptyset$ \Comment{Set of Payload Items with ssn}
    \State $\tuple{ssn_s, rd_s} \gets record_s$
    \State $\tuple{mid_s, vc_s, hmac_s, payload_s} \gets rd_s$\\
    
    \ForAll{$payloadItems$ in $payload_s$}
        \State $PISSN \gets PISSN \cup \tuple{payloadItem, ssn_s}$
    \EndFor\\
    
    \State \Return {$PISSN$}
\EndFunction
\end{algorithmic}
\end{varwidth}% 
}

%Get rid For Record
\noindent\fbox{%
\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}
\textbf{Get rid For Record}:
\begin{algorithmic}[1]
\Function{GetRid}{$record_s$}
    \State $\tuple{ssn_s, \tuple{mid_s, \{c_{mid_1}, c_{mid_2}, ... , c_{mid_k}\}, hmac_s, payload_s}} \gets record_s$
    \State \Return {$\tuple{mid_s, c_{mid_s}}$}
\EndFunction
\end{algorithmic}
\end{varwidth}% 
}


\textbf{Get Transaction Arbitrator}:\\
\textbf{Transaction Live}:\\
\textbf{Commit Live}:\\

%Sequence Live
\noindent\fbox{%
\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}
\textbf{Sequence Live}:
\begin{algorithmic}[1]
\Function{SequenceLive}{$sequence_s, ssn_{s1}$}
    \State $API \gets \emptyset$   \Comment{Set of all Payload Items}
    \State $AS \gets \emptyset$    \Comment{Set of all Payload Items that are sequences}
    \State $StillHasRecord \gets False$
    \State $\tuple{rid_s, ssn_{s2}} \gets sequence_s$\\
    
    \ForAll{$record$ in $R$}
        \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record}
        \If{$rid_s = $\Call{GetRid}{$record$}}
            \State $StillHasRecord \gets True$
        \EndIf
    \EndFor\\
    
    \If{$\lnot StillHasRecord$}  \Comment{The Record does not exists anymore}
        \State \Return{False}
    \EndIf\\
    
    \ForAll{$\tuple{ssn, payload}$ in $API$}
        \If{$payload$ is a $sequence$}
            \State $AS \gets AS \cup \{\tuple{ssn, payload}\}$   \Comment{Extract all sequence payloads}
        \EndIf
    \EndFor\\
    
    \ForAll{$\tuple{ssn_1', \tuple{rid', ssn_2'}}$ in $AS$}
        \If{$(rid'=rid_s) \land (ssn_1' > ssn_{s_1})$}
            \State \Return{False}
        \EndIf
    \EndFor \\
    \State \Return{True}
\EndFunction
\end{algorithmic}
\end{varwidth}% 
}

% Delete Live
\noindent\fbox{%
\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}
\textbf{Delete Live}:
\begin{algorithmic}[1]
\Function{DeleteLive}{$delete_s, ssn_s$}
    \State $API \gets \emptyset$   \Comment{Set of all Payload Items}
    \State $AD \gets \emptyset$    \Comment{Set of all Payload Items that are deletes}
    \State $\tuple{ssn_d} \gets delete_s$\\
    
    \ForAll{record in R}
        \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record}
    \EndFor\\
    
    \ForAll{$\tuple{ssn, payload}$ in $API$}
        \If{$payload$ is a $delete$}
            \State $AD \gets AD \cup \{\tuple{ssn, payload}\}$   \Comment{Extract all delete payloads}
        \EndIf
    \EndFor\\
    
    \ForAll{delete in AD}
        \State $\tuple{{ssn_s}', \tuple{{ssn_d}'}} \gets delete$
        \If{${ssn_d}' > ssn_d$}    \Comment{More recently deleted record}
            \State \Return{False}
        \ElsIf{$({ssn_d}'= ssn_d) \land ({ssn_s}' > ssn_s)$} \Comment{More recent delete of same record}
            \State \Return{False}
        \EndIf
    \EndFor \\
    \State \Return{True}
\EndFunction
\end{algorithmic}
\end{varwidth}% 
}

%Abort Live
\noindent\fbox{%
\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}
\textbf{Abort Live}:
\begin{algorithmic}[1]
\Function{AbortLive}{$abort_s$}
    \State $\tuple{tid_s,mid_s,vc_s} \gets abort_s$\\
    \ForAll{record in R}
        \State $\tuple{ssn_s',\tuple{mid_s', vc_s', hmac_s', payload_s'}} \gets record$
        \If{$(mid_s'=mid_s) \land (vc_s' > vc_s)$}
            \State \Return{True}
        \EndIf
    \EndFor\\
    \State \Return{False}
\EndFunction
\end{algorithmic}
\end{varwidth}% 
}

%Resize Live
\noindent\fbox{%
\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}
\textbf{Resize Live}:
\begin{algorithmic}[1]
\Function{ResizeLive}{$resize_s, ssn_s$}
    \State $API \gets \emptyset$   \Comment{Set of all Payload Items}
    \State $AR \gets \emptyset$    \Comment{Set of all Payload Items that are resize}
    \State $\tuple{size} \gets resize_s$\\
    
    \ForAll{record in R}
        \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record}
    \EndFor\\
    
    \ForAll{$\tuple{ssn, payload}$ in $API$}
        \If{$payload$ is a $resize$}
            \State $AR \gets AR \cup \{\tuple{ssn, payload}\}$   \Comment{Extract all resize payloads}
        \EndIf
    \EndFor\\
    
    \ForAll{$\tuple{ssn', \tuple{size'}}$ in $AR$}
        \If{$size' > size$}
            \State \Return{False}
        \ElsIf{$(size'=size) \land (ssn' > ssn_s)$}
            \State \Return{False}
        \EndIf
    \EndFor \\
    \State \Return{True}
\EndFunction
\end{algorithmic}
\end{varwidth}% 
}



\textbf{Evaluate Guard Condition:}\\


\textbf{Get Latest Data Structure From Server:}\\
\textbf{Delete Records:}\\
\textbf{Check Data Structure for Malicious Activity:}


\subsection{\textbf{Put Transaction}}



\subsection{\textbf{Get key-value pair}}
\subsection{\textbf{Create new key}}

\end{document}
