--- a/provsec/paper.tex	Mon Apr 12 13:00:57 2010 +0200
+++ b/provsec/paper.tex	Mon Apr 12 15:18:29 2010 +0200
@@ -558,8 +558,58 @@
 \end{verbatim}
 
 Notice that we need to take special care that the temporary variables
-\verb|a_then0|, \verb|cond0| etc.\ are not combined in the second step,
+\verb|a_then0|, \verb|cond0| etc.\ are\emph{not}\/ combined in the second step,
 as they will never by used outside the transformed if.
+
+Here follows a description of the algorithm used for the rewrite:
+
+If the condition of an if statement is secret, we go through the statements of each branch in turn and do as follows:
+\begin{enumerate}
+\item If the statement is an assignment, we look up if we have assigned to that specific variable before during the current branch:
+  \begin{enumerate}
+  \item If the assignment not synthesized during a recursive
+    invocation of the procedure we do not need it outside this branch,
+    and nothing needs to be changes, so we leave it in place.
+  \item Otherwise, if we have not assigned to this variable before; we
+    suffix the assigned variable name with a fresh \verb|_thenx| (or
+    \verb|_elsex|) and remember this renaming.
+  \item If we have assigned to this variable before in the same branch
+    we reuse the same name as last time.
+  \item All variables on the right-hand side that have been renamed in
+    previous assignments, are updated to their new name.
+  \end{enumerate}
+\item If the statement is an if-statement we rename variables in its
+  condition, and apply the algorithm recursively, so it becomes a list
+  of straight-line assignments, we then continue the rewriting through
+  these. But we only compute branch-specific values for those that are
+  not synthesized.
+\item If the statement is a \verb|pass| we leave it.
+\item Other statements trigger an error.
+\end{enumerate}
+The updated statements first from the \emph{then}\/ and then from the
+\emph{else}\/ branch are emitted in place of the if statement. 
+
+Now we have computed in variables suffixed with \verb|_then| the value
+of variables as they would be if \verb|cond|=1, and in those suffixed
+\verb|_else| what they would be if \verb|cond|=0.
+
+Finally we emit statements for obliviously combining the values of the
+variables of the two branches. These are one assignment for each
+variable that is assigned to, in at least one of the branches. If it
+occurs only in one branch we use the original name for the variable
+for that branch. Then we combine them as follows:
+
+\verb|a = a_else + (a_then - a_else) * cond|
+
+Because the range-analysis guarantees us that \verb|cond| is in $\{0,1\}$ this will give the right value of a.
+
+One subtlety is that function calls are made no matter what the
+condition was, this might give counter-intuitive results, because
+side-effects will happen no matter what branch was chosen --- we leave
+this up to the programmer, as we do not have the infrastructure for
+forbidding side-effects, but function-calls are nice to be able to
+make in the branches.
+%TODO: Maybe it is better to emit an error, and suggest the function call is moved before the assignment?
 \subsection{Output and Timing of Operations}
 We compile PySMCL into VIFF programs. VIFF uses a system of
 ``deferreds'' to give the impression of programming a synchronous