fix packing + more writing

Makefile

@@ -37,9 +37,11 @@ coq-tweetnacl-vst: coq-tweetnacl-spec .building2
 clean-vst: P=proofs/vst
 clean-vst: .dusting2
 
+.PHONY: clean
 clean: clean-spec clean-vst clean-dist
 
 # build paper
+.PHONY: paper
 paper:
 	cd paper && $(MAKE)
 

paper/highlevel.tex

@@ -305,25 +305,25 @@ In the case of X25519, $n$ is the private key. With the Montgomery's ladder, whi
 it provides slightly more computations and an extra variable, we can prevent such weakness.
 See Algorithm \ref{montgomery-ladder}.
 
-\begin{algorithm}
-\caption{Montgomery ladder for scalar mult.}
-\label{montgomery-ladder}
-\begin{algorithmic}
-\REQUIRE{Point $P$, scalars $n$ and $m$, $n < 2^m$}
-\ENSURE{$Q = n \cdot P$}
-\STATE $Q \leftarrow \Oinf$
-\STATE $R \leftarrow P$
-\FOR{$k$ := $m$ downto $1$}
-  \IF{$k^{\text{th}}$ bit of $n$ is $0$}
-    \STATE $R \leftarrow Q + R$
-    \STATE $Q \leftarrow 2Q$
-  \ELSE
-    \STATE $Q \leftarrow Q + R$
-    \STATE $R \leftarrow 2R$
-  \ENDIF
-\ENDFOR
-\end{algorithmic}
-\end{algorithm}
+% \begin{algorithm}
+% \caption{Montgomery ladder for scalar mult.}
+% \label{montgomery-ladder}
+% \begin{algorithmic}
+% \REQUIRE{Point $P$, scalars $n$ and $m$, $n < 2^m$}
+% \ENSURE{$Q = n \cdot P$}
+% \STATE $Q \leftarrow \Oinf$
+% \STATE $R \leftarrow P$
+% \FOR{$k$ := $m$ downto $1$}
+%   \IF{$k^{\text{th}}$ bit of $n$ is $0$}
+%     \STATE $R \leftarrow Q + R$
+%     \STATE $Q \leftarrow 2Q$
+%   \ELSE
+%     \STATE $Q \leftarrow Q + R$
+%     \STATE $R \leftarrow 2R$
+%   \ENDIF
+% \ENDFOR
+% \end{algorithmic}
+% \end{algorithm}
 
 \begin{lemma}
 \label{lemma-montgomery-ladder}

paper/preliminaries.tex

@@ -41,19 +41,11 @@ such coordinates are represented as $X/Z$ fractions. We define two operations:
 \texttt{xADD} &: (X_P, Z_P, X_Q , Z_Q, X_{P-Q}, Z_{P-Q}) \mapsto (X_{P+Q}, Z_{P+Q})\\
 \texttt{xDBL} &: (X_P, Z_P) \mapsto (X_{2P}, Z_{2P})\\
 \end{align*}
-To remove secret-dependent if-statements we use a constant-time conditional swap
-(see Algorithm~\ref{c-swap}).
-\begin{algorithm}
-\caption{\texttt{SWAP} : Constant-time conditional swap}
-\label{c-swap}
-\begin{algorithmic}
-\REQUIRE{$b \in \{0, 1\}$ and a pair $(X_0, X_1)$ of objects encoded as $n$-bit strings}
-\ENSURE{$(X_b, X_{1-b})$}
-\STATE $B \leftarrow (b, \ldots, b)_n$
-\STATE $Mask \leftarrow B \texttt{ AND } (X_0\texttt{ XOR } X_1)$
-\RETURN $(X_0 \texttt{ XOR } Mask, X_1 \texttt{ XOR } Mask)$
-\end{algorithmic}
-\end{algorithm}
+In the Montgomery, notice that the arguments of \texttt{xADD} and \texttt{xDBL}
+are swapped depending of the value of the $k^{th}$ bit. We use a conditional
+swap \texttt{CSWAP} to change the arguments of the above function. This  while keeping the same body of the loop.
+Given a pair $(X_0, X_1)$ and a boolean $b$, \texttt{CSWAP} returns the pair
+$(X_b, X_{1-b})$.
 
 By using the differential addition and doubling operations we define the Montgomery ladder
 computing a $x$-coordinate-only scalar multiplication (see Algorithm~\ref{montgomery-ladder}).
@@ -66,10 +58,10 @@ computing a $x$-coordinate-only scalar multiplication (see Algorithm~\ref{montgo
 \STATE $Q \leftarrow \Oinf$
 \STATE $R \leftarrow (X_P,Z_P)$
 \FOR{$k$ := $m$ down to $1$}
-  \STATE $(Q,R) \leftarrow \texttt{SWAP}(k^{\text{th}}\text{ bit of }n, (Q,R))$
+  \STATE $(Q,R) \leftarrow \texttt{SWAP}((Q,R), k^{\text{th}}\text{ bit of }n)$
   \STATE $Q \leftarrow \texttt{xDBL}(Q)$
   \STATE $R \leftarrow \texttt{xADD}(Q,R,X_P,Z_P)$
-  \STATE $(Q,R) \leftarrow \texttt{SWAP}(k^{\text{th}}\text{ bit of }n, (Q,R))$
+  \STATE $(Q,R) \leftarrow \texttt{SWAP}((Q,R), k^{\text{th}}\text{ bit of }n)$
 \ENDFOR
 \RETURN $Q$
 \end{algorithmic}
@@ -212,20 +204,20 @@ It takes the exponentiation by $2^{255}-21$ with the Square-and-multiply algorit
 Fermat's little theorem brings the correctness.
 Notice that in this case the inverse of $0$ is defined as $0$.
 
-\TNaCle{sel25519} implements a constant-time conditional \texttt{SWAP} (Algorithm~\ref{c-swap})
+\TNaCle{sel25519} implements a constant-time conditional \texttt{CSWAP} (Algorithm~\ref{c-swap})
 by applying a mask between two fields elements.
-% \begin{lstlisting}[language=Ctweetnacl]
-% sv sel25519(gf p,gf q,i64 b)
-% {
-%   int i;
-%   i64 t,c=~(b-1);
-%   FOR(i,16) {
-%     t= c&(p[i]^q[i]);
-%     p[i]^=t;
-%     q[i]^=t;
-%   }
-% }
-% \end{lstlisting}
+\begin{lstlisting}[language=Ctweetnacl]
+sv sel25519(gf p,gf q,i64 b)
+{
+  int i;
+  i64 t,c=~(b-1);
+  FOR(i,16) {
+    t= c&(p[i]^q[i]);
+    p[i]^=t;
+    q[i]^=t;
+  }
+}
+\end{lstlisting}
 
 Finally, we require the \TNaCle{pack25519} function,
 which converts from the internal redundant radix-$2^{16}$

proofs/vst/c/tweetnaclVerifiableC.c

@@ -310,7 +310,7 @@ sv pack25519(u8 *o,const gf n)
     }
     m[15]=t[15]-0x7fff-((m[14]>>16)&1);
     m[14]&=0xffff;
-    b=1-(m[15]>>16)&1;
+    b=1-((m[15]>>16)&1);
     sel25519(t,m,b);
   }
   FOR(i,16) {