Documenting adv, getTime, and random

Author: Aslan Askarov

body.tex

@@ -320,7 +320,7 @@ \section{Information flow control}
 levels. The security level of 
 a value specifies the confidentiality policy of the 
 value. Troupe uses the syntax \textcode{$\mathit{v}$@\lev{$\mathit{\ell_{\mathit{val}}}$}\%\lev{$\mathit{\ell_{\mathit{type}}}$}} to 
-for denote that the value $\mathit{v}$ has security level 
+denote that the value $\mathit{v}$ has security level 
 $\mathit{\ell_{\mathit{val}}}$, and the information about the type of this value is labeled at $\mathit{\ell_{\mathit{type}}}$.
 
 
@@ -583,12 +583,13 @@ \subsubsection{Generalized receive and mailbox clearances}
 care needs to be taken to control information flows through the mailbox structure.
 
 
-Every message in a mailbox carries an extra label -- the blocking level of the sender.
-Receiving a value furthermore propagates the taint of the blocking level from the sender to the receiver. 
+Every message in a mailbox carries an extra label -- the blocking level of the sender. We refer to this 
+extra label as the \emph{presence label}.
+Receiving a value furthermore propagates the taint of the blocking level from the sender to the receiver via the presence label. 
 In order to constrain a receive operation from an accidental raise of the blocking level, Troupe
 provides a general receive primitive in the form 
 \code{rcv(lev1,lev2,hns)}. Here, \code{lev1} and \code{lev2}
-indicate the to and from-levels of the pc-tags on the messages, and \code{hns} is the list of 
+indicate the to and from-levels of the presence labels on the messages, and \code{hns} is the list of 
 handlers as before.
 The \code{receive} operation we introduced earlier is equivalent to \code{rcvp}
 at the level of the current pc label.
@@ -598,8 +599,9 @@ \subsubsection{Generalized receive and mailbox clearances}
 
 
 \begin{lstlisting}
-let val _ = if (secret) then rcv ({}, {alice}, [hn x => x] else ()
-in val x = rcv ({}, {}, [hn x => x ])
+let val _ = if secret then rcv ({}, {alice}, [hn x => x])
+                      else ()
+in rcv ({}, {}, [hn x => x])
 end
 \end{lstlisting}
 
@@ -719,12 +721,22 @@ \section{Language reference}
 
 \subsection{Built-in expressions}
 
+\subsubsection{\code{adv}}
+\begin{description}
+    \item [Description] Simulate sending a value to adversary at level $\{\}$. This function is introduced as a 
+    pedagogical convenience as as it removes the necessity to set up a network process when explaining explicit and implicit information flows.
+    \item [Arguments] A value to pass to the adversary.
+    \item [Returns] Unit.
+    \item [Failure behavior] Crashes the current process if the provided value and the blocking label are more restrictive than bottom.
+    \item [Example usage] \code{adv\ (42\ raisedTo\ \{alice\})}. 
+\end{description}
+
 \subsubsection{\code{attenuate}}
 \begin{description}
     \item [Description] Returns the attenuated authority 
     \item [Arguments] A value of authority type.
     \item [Returns] A value of authority type
-    \item [Example usage] \code{attenuate ( authority, \{alice\} ) }
+    \item [Example usage] \code{attenuate ( authority, \{alice\} ) } Note that the above example will generate a runtime error.
 \end{description}
 
 
@@ -758,6 +770,16 @@ \subsubsection{\code{declassify}}
 
 \end{description}
 
+
+\subsubsection{\code{getTime}}
+\begin{description}
+    \item [Description] Obtains current Unix timestmap
+    \item [Arguments] Unit.
+    \item [Returns] Number. 
+    \item [Example usage] \textcode{getTime()}
+\end{description}
+
+
 \subsubsection{\code{lowermbox}}
 \begin{description}
     \item [Description] Lowers the clearance of the current process' mailbox. 
@@ -810,6 +832,16 @@ \subsubsection{\code{printWithLabels}}
     \item [Example usage] \code{printWithLabels\ "Hello, world"}
 \end{description}
 
+\subsubsection{\code{random}}
+\begin{description}
+    \item [Description] Generates a random number between 0 (inclusive) and 1.
+    \item [Arguments] Unit.
+    \item [Returns] Number.
+    \item [Example usage] \code{random()}
+\end{description}
+
+
+
 \subsubsection{\code{sandbox}} 
 \begin{description}
     \item [Description] Execute a function in a sandbox for a fixed duration of time.
@@ -972,12 +1004,12 @@ \subsubsection{\code{whereis}}
 \end{minipage}
 \end{description}
 
-
 \clearpage
 \section{Installation and configuration}
 \label{appendix:installationandconfig}
 \subsection{Installation}
-See also the {\tt README} file provided with the installation.
+See the {\tt README} file provided with the installation.
+\if 0
 \begin{enumerate}
     \item Install Node JS.\footnote{
     See \url{https://www.digitalocean.com/community/tutorials/how-to-install-node-js-on-ubuntu-18-04}}
@@ -986,14 +1018,14 @@ \subsection{Installation}
     \item Check that the compiler works by running the local test suite: {\tt \$TROUPE/bin/golden}
     \item If you get a message saying that all tests have passed, this means that the local tests work. You can now test the distributed runtime by trying out the Echo example.
 \end{enumerate}
+\fi
 
-\subsection{Create a network identifier for your server}
+
+\subsection{Configuring network identifiers}
 \label{sec:networkid}
 Create a network identifier (together with the public/private key pair) for your node. 
 \begin{verbatim}
-$ mkdir -p code/ids
-$ cd code/ids/
-$ curl lbs-troupe.troupe-lang.org/mkid -o id-server.json
+$ curl lbs-troupe.troupe-lang.org/mkid -o my-identifier.json
 \end{verbatim}
 
 The {\tt "id"} section of the JSON file is your identifier. The other 
@@ -1002,16 +1034,6 @@ \subsection{Create a network identifier for your server}
 
 
 \subsubsection{Testing your network identifier (optional)}
-At this step, you can pass the file \verb+id-server.json+ 
-when passing it as an argument to Troupe runtime. For example,
-you can use this to try out the Echo example from Section~\ref{example:echo}. For this,
-do the following steps.
-\begin{enumerate}
-\item Make sure the {\tt id-server.json} file is in the {\tt code/ids/} directory.
-\item Edit {\tt echo-client.trp} by substituting the identity of the server for your own.
-\item Run {\tt make echo-server}.
-\item Open another terminal and run {\tt make echo-client}. If all works, you should see the output from the server.
-\end{enumerate}
-You can interrupt the execution with \^{}C.
-
-
+At this step, you can pass the generated JSON file
+as an argument to Troupe runtime, using the \verb+--id+ flag. See 
+the echo example provided with the installation.

main.tex

@@ -38,7 +38,8 @@
 
 %\author{}
 % \author{\sf Aslan Askarov \\ \small aslan@cs.au.dk}
-%\date{}  % Activate to display a given date or no date
+
+\date{March 4, 2020}  % Activate to display a given date or no date
 
 \begin{document}
 \maketitle