\subsection{The X25519 key exchange} \label{subsec:X25519-key-exchange} From now on let $\F{p}$ be the field with $p=2^{255}-19$ elements. We consider the elliptic curve $E$ over $\F{p}$ defined by the equation $y^2 = x^3 + 486662 x^2 + x$. For every $x \in \F{p}$ there exists a point $P$ in $E(\F{p^2})$ such that $x$ is the \xcoord of $P$. The core of the X25519 key-exchange protocol is a scalar\hyp{}multiplication function, which we will also refer to as X25519. This function receives as input two arrays of $32$ bytes each. One of them is interpreted as the little-endian encoding of a non-negative 256-bit integer $n$ (see \ref{sec:Coq-RFC}). The other is interpreted as the little-endian encoding of the \xcoord $x_P \in \F{p}$ of a point in $E(\F{p^2})$, using the standard mapping of integers modulo $p$ to elements in $\F{p}$. The X25519 function first computes a scalar $n'$ from $n$ by setting bits at position 0, 1, 2 and 255 to \texttt{0}; and at position 254 to \texttt{1}. This operation is often called clamping'' of the scalar $n$. Note that $n' \in 2^{254} + 8\{0,1,\ldots,2^{251}-1\}$. X25519 then computes the \xcoord of $n'\cdot P$. RFC~7748~\cite{rfc7748} standardizes the X25519 Diffieâ€“Hellman key-exchange algorithm. Given the base point $B$ where $X_B=9$, each party generates a secret random number $s_a$ (respectively $s_b$), and computes $X_{P_a}$ (respectively $X_{P_b}$), the \xcoord of $P_A = s_a \cdot B$ (respectively $P_B = s_b \cdot B$). The parties exchange $X_{P_a}$ and $X_{P_b}$ and compute their shared secret $s_a \cdot s_b \cdot B$ with X25519 on $s_a$ and $X_{P_b}$ (respectively $s_b$ and $X_{P_a}$).