\section{Proving that X25519 in Coq matches the mathematical model}
\label{sec:maths}

In this section we prove the following informal theorem:

\begin{informaltheorem}
  The implementation of X25519 in TweetNaCl computes the
  $\F{p}$-restricted \xcoord scalar multiplication on $E(\F{p^2})$ where $p$ is $\p$
  and $E$ is the elliptic curve $y^2 = x^3 + 486662 x^2 + x$.
\end{informaltheorem}

More precisely, we prove that our formalization of the RFC matches the definitions of Curve25519 by Bernstein:
\begin{lstlisting}[language=Coq]
Theorem RFC_Correct: forall (n p : list Z)
  (P:mc curve25519_Fp2_mcuType),
  Zlength n = 32 ->
  Zlength p = 32 ->
  Forall (fun x => 0 <= x /\ x < 2 ^ 8) n ->
  Forall (fun x => 0 <= x /\ x < 2 ^ 8) p ->
  Fp2_x (decodeUCoordinate p) = P#x0 ->
  RFC n p =
    encodeUCoordinate
      ((P *+ (Z.to_nat (decodeScalar25519 n))) _x0).
\end{lstlisting}

We first review the work of Bartzia and Strub \cite{BartziaS14} (\ref{subsec:ECC-Weierstrass}).
We extend it to support Montgomery curves (\ref{subsec:ECC-Montgomery})
with projective coordinates (\ref{subsec:ECC-projective}) and prove the
correctness of the ladder (\ref{subsec:ECC-ladder}).
We discuss the twist of Curve25519 (\ref{subsec:Zmodp}) and explain how we deal
with it in the proofs (\ref{subsec:curvep2}).

\subsection{Formalization of elliptic curves}
\label{subsec:ECC}

\fref{tikz:ProofHighLevel1} presents the structure of the proof of the ladder's
correctness. The white tiles are definitions, the orange ones are hypothesis and
the green tiles represent major lemmas and theorems.

% The plan is as follows.
% (This is part of the description of the picture).
We consider the field $\K$ and formalize the Montgomery curves ($M_{a,b}(\K)$).
Then, by using the equivalent Weierstra{\ss} form ($E_{a',b'}(\K)$) from the library of Bartzia and Strub,
we prove that $M_{a,b}(\K)$ forms an commutative group.
Under the hypothesis that
$a^2 - 4$ is not a square in $\K$, we prove the correctness of the ladder (\tref{thm:montgomery-ladder-correct}).

\begin{figure}[h]
  \centering
  \include{tikz/highlevel1}
  \vspace{-0.5cm}
  \caption{Overview of the proof of Montgomery ladder's correctness}
  \label{tikz:ProofHighLevel1}
\end{figure}

% this is for the flow of the text otherwise someone will again complain of a definition poping out of nowhere.
We now turn our attention to the details of the proof of the ladder's correctness.

\begin{dfn}
  Given a field $\K$,
  using an appropriate choice of coordinates,
  an elliptic curve $E$
  is a plane cubic algebraic curve defined by an equation $E(x,y)$ of the form:
  $$E : y^2 + a_1 xy + a_3 y = x^3 + a_2 x^2 + a_4 x + a_6$$
  where the $a_i$'s are in \K\ and the curve has no singular point (\ie no cusps
  or self-intersections). The set of points defined over \K, written $E(\K)$, is formed by the
  solutions $(x,y)$ of $E$ together with a distinguished point $\Oinf$ called point at infinity:
  $$E(\K) = \{ (x,y) \in \K \times \K ~|~E(x,y)\} \cup \{\Oinf\}$$
\end{dfn}

\subsubsection{Short Weierstra{\ss} curves}
\label{subsec:ECC-Weierstrass}

For the remainder of this text, we assume that the characteristic of $\K$ is neither 2 nor 3.
Then, this equation $E(x,y)$ can be reduced into its short Weierstra{\ss} form.

\begin{dfn}
  Let $a \in \K$ and $b \in \K$ such that $$\Delta(a,b) = -16(4a^3 + 27b^2) \neq 0.$$
  The \textit{elliptic curve} $E_{a,b}$ is defined by the equation
  $$y^2 = x^3 + ax + b.$$
  $E_{a,b}(\K)$ is the set of all points $(x,y) \in \K^2$ satisfying the $E_{a,b}$
  along with an additional formal point $\Oinf$, ``at infinity''. Such a curve does not have any singularity.
\end{dfn}

In this setting, Bartzia and Strub defined the parametric type \texttt{ec} which
represents the points on a specific curve. It is parameterized by
a \texttt{K : ecuFieldType} ---the type of fields whose characteristic is neither 2 nor 3---
and \texttt{E : ecuType} ---a record that packs the curve parameters $a$ and $b$---
along with the proof that $\Delta(a,b) \neq 0$.
\begin{lstlisting}[language=Coq]
Inductive point := EC_Inf | EC_In of K * K.
Notation "(| x, y |)" := (EC_In x y).
Notation "\infty" := (EC_Inf).

Record ecuType :=
  { A : K; B : K; _ : 4 * A^3 + 27 * B^2 != 0}.
Definition oncurve (p : point) :=
  if p is (| x, y |)
    then y^2 == x^3 + A * x + B
    else true.
Inductive ec : Type := EC p of oncurve p.
\end{lstlisting}

Points on an elliptic curve form an abelian group when equipped with the following structure.%
\begin{itemize}
  \item The negation of a point $P = (x,y)$ is defined by reflection over the $x$-axis, \ie $-P = (x, -y)$.
  \item The addition of two points $P$ and $Q$ is defined as the negation of the third intersection point
        of the line passing through $P$ and $Q$, or tangent to $P$ if $P = Q$.
  \item $\Oinf$ is the neutral element under this law: if 3 points are collinear, their sum is equal to $\Oinf$
\end{itemize}
These operations are defined in Coq as follows (where we omit the code for the tangent case):
\begin{lstlisting}[language=Coq]
Definition neg (p : point) :=
  if p is (| x, y |) then (| x, -y |) else EC_Inf.

Definition add (p1 p2 : point) :=
  match p1, p2 with
    | \infty , _ => p2
    | _ , \infty => p1
    | (| x1, y1 |), (| x2, y2 |) =>
      if x1 == x2 then ... else
        let s := (y2 - y1) / (x2 - x1) in
        let xs := s^2 - x1 - x2 in
          (| xs, - s * (xs - x1 ) - y1 |)
  end.
\end{lstlisting}
The value of \texttt{add} is proven to be on the curve with coercion:
\begin{lstlisting}[language=Coq]
Lemma addO (p q : ec): oncurve (add p q).

Definition addec (p1 p2 : ec) : ec :=
  EC p1 p2 (addO p1 p2)
\end{lstlisting}

\subsubsection{Montgomery curves}
\label{subsec:ECC-Montgomery}

Speedups can be obtained by switching to projective coordinates and other forms
than the Weierstra{\ss} form. We consider the Montgomery form \cite{MontgomerySpeeding}.

\begin{dfn}
  Let $a \in \K \backslash \{-2, 2\}$, and $b \in \K \backslash \{ 0\}$.
  The \textit{elliptic curve} $M_{a,b}$ is defined by the equation:
  $$by^2 = x^3 + ax^2 + x,$$
  $M_{a,b}(\K)$ is the set of all points $(x,y) \in \K^2$ satisfying the $M_{a,b}$
  along with an additional formal point $\Oinf$, ``at infinity''.
\end{dfn}
Similar to the definition of \texttt{ec}, we define the parametric type \texttt{mc} which
represents the points on a specific Montgomery curve.
It is parameterized by
a \texttt{K : ecuFieldType} ---the type of fields whose characteristic is neither
2 nor 3--- and \texttt{M : mcuType} ---a record that packs the curve
parameters $a$ and $b$ along with the proofs that $b \neq 0$ and $a^2 \neq 4$.
\begin{lstlisting}[language=Coq,belowskip=-0.1 \baselineskip]
Record mcuType :=
  { cA : K; cB : K; _ : cB != 0; _ : cA^2 != 4}.
Definition oncurve (p : point K) :=
if p is (| x, y |)
  then cB * y^+2 == x^+3 + cA * x^+2 + x
  else true.
Inductive mc : Type := MC p of oncurve p.

Lemma oncurve_mc: forall p : mc, oncurve p.
\end{lstlisting}
We define the addition on Montgomery curves in a similar way as for the Weierstra{\ss} form.
\begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
Definition add (p1 p2 : point K) :=
  match p1, p2 with
    | \infty, _ => p2
    | _, \infty => p1
    | (|x1, y1|), (|x2, y2|) =>
      if   x1 == x2
      then if  (y1 == y2) && (y1 != 0)
           then ... else \infty
      else
        let s  := (y2 - y1) / (x2 - x1) in
        let xs := s^+2 * cB - cA - x1 - x2 in
          (| xs, - s * (xs - x1) - y1 |)
    end.
\end{lstlisting}
And again we prove the result is on the curve:
\begin{lstlisting}[language=Coq]
Lemma addO (p q : mc) : oncurve (add p q).

Definition addmc (p1 p2 : mc) : mc :=
  MC p1 p2 (addO p1 p2)
\end{lstlisting}

We define a bijection between a Montgomery curve and its short Weierstra{\ss} form
(\lref{lemma:bij-ecc}) and prove that it respects the addition as defined on the
respective curves. In this way we get all the group laws for Montgomery curves from the Weierstra{\ss} ones.

After having verified the group properties, it follows that the bijection is a group isomorphism.
\begin{lemma}
  \label{lemma:bij-ecc}
  Let $M_{a,b}$ be a Montgomery curve, define
  \vspace{-0.3em}
  $$a' = \frac{3-a^2}{3b^2} \text{\ \ \ \ and\ \ \ \ } b' = \frac{2a^3 - 9a}{27b^3}.$$
  then $E_{a',b'}$ is a Weierstra{\ss} curve, and the mapping
  $\varphi : M_{a,b} \mapsto E_{a',b'}$ defined as:
  \vspace{-0.5em}
  \begin{align*}
    \varphi(\Oinf_M)   & = \Oinf_E                                                 \\[-0.5ex]
    \varphi( (x , y) ) & = \left( \frac{x}{b} + \frac{a}{3b} , \frac{y}{b} \right)
  \end{align*}
  is a group isomorphism between elliptic curves.
\end{lemma}
% \begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
% Definition ec_of_mc_point p :=
%   match p with
%   | \infty => \infty
%   | (|x, y|) => (|x/(M#b) + (M#a)/(3%:R * (M#b)), y/(M#b)|)
%   end.
% Lemma ec_of_mc_point_ok p :
%   oncurve M p ->
%   ec.oncurve E (ec_of_mc_point p).

% Definition ec_of_mc p :=
%   EC (ec_of_mc_point_ok (oncurve_mc p)).

% Lemma ec_of_mc_bij : bijective ec_of_mc.
% \end{lstlisting}

\subsubsection{Projective coordinates}
\label{subsec:ECC-projective}

In a projective plane, points are represented by the triples $(X:Y:Z)$ excluding $(0:0:0)$.
Scalar multiples of triples are identified with each other, \ie
for all $\lambda \neq 0$, the triples $(X:Y:Z)$ and $(\lambda X:\lambda Y:\lambda Z)$ represent
the same point in the projective plane.
For $Z\neq 0$, the point $(X:Y:Z)$ corresponds to the
point $(X/Z,Y/Z)$ in the affine plane.
Likewise, the point $(X,Y)$ in the affine plane corresponds to $(X:Y:1)$ in the projective plane.
% The points $(X : Y : 0)$ can be considered as points at infinity.

Using fractions as coordinates, the equation for a Montgomery curve $M_{a,b}$
becomes
$$b \bigg(\frac{Y}{Z}\bigg)^2 = \bigg(\frac{X}{Z}\bigg)^3 + a \bigg(\frac{X}{Z}\bigg)^2 + \bigg(\frac{X}{Z}\bigg).$$
Multiplying both sides by $Z^3$ yields
$$b Y^2Z = X^3 + a X^2Z + XZ^2.$$
Setting $Z = 0$ in this equation, we derive $X = 0$.
Hence, $(0 : 1 : 0)$ is the unique point on the curve at infinity.

By restricting the parameter $a$ of $M_{a,b}(\K)$ such that $a^2-4$ is not a
square in \K (Hypothesis \ref{hyp:a_minus_4_not_square}),
we ensure that $(0,0)$ is the only point with a $y$-coordinate of $0$.
\begin{hypothesis}
  \label{hyp:a_minus_4_not_square}
  The number $a^2-4$ is not a square in \K.
\end{hypothesis}
\begin{lstlisting}[language=Coq]
Hypothesis mcu_no_square :
  forall x : K, x^+2 != (M#a)^+2 - 4%:R.
\end{lstlisting}

We define $\chi$ and $\chi_0$ to return the \xcoord of points on a curve.
\begin{dfn}
  Let $\chi : M_{a,b}(\K) \mapsto \K \cup \{\infty\}$ and $\chi_0 : M_{a,b}(\K) \mapsto \K$ such that
  \vspace{-0.5em}
  \begin{align*}
    \chi((x,y))   & = x, & \chi(\Oinf)   & = \infty, &  & \text{and} \\[-0.5ex]
    \chi_0((x,y)) & = x, & \chi_0(\Oinf) & = 0.
  \end{align*}
\end{dfn}

Using projective coordinates we prove the formula for differential addition.% (\lref{lemma:xADD}).
\begin{lemma}
  \label{lemma:xADD}
  Let $M_{a,b}$ be a Montgomery curve such that $a^2-4$ is not a square in \K, and
  let $X_1, Z_1, X_2, Z_2, X_4, Z_4 \in \K$, such that $(X_1,Z_1) \neq (0,0)$,
  $(X_2,Z_2) \neq (0,0)$, $X_4 \neq 0$ and $Z_4 \neq 0$.
  Define
  \vspace{-0.5em}
  \begin{align*}
    X_3 & = Z_4((X_1 - Z_1)(X_2+Z_2) + (X_1+Z_1)(X_2-Z_2))^2 \\[-0.5ex]
    Z_3 & = X_4((X_1 - Z_1)(X_2+Z_2) - (X_1+Z_1)(X_2-Z_2))^2
  \end{align*}
  then for any point $P_1$ and $P_2$ in $M_{a,b}(\K)$ such that
  $X_1/Z_1 = \chi(P_1), X_2/Z_2 = \chi(P_2)$, and $X_4/Z_4 = \chi(P_1 - P_2)$,
  we have $X_3/Z_3 = \chi(P_1+P_2)$.\\
  \textbf{Remark:}
  These definitions should be understood in $\K \cup \{\infty\}$.
  If $x\ne 0$ then we define $x/0 = \infty$.
\end{lemma}
Similarly, we also prove the formula for point doubling.% (\lref{lemma:xDBL}).
\begin{lemma}
  \label{lemma:xDBL}
  Let $M_{a,b}$ be a Montgomery curve such that $a^2-4$ is not a square in \K, and
  let $X_1, Z_1 \in \K$, such that $(X_1,Z_1) \neq (0,0)$. Define
  \begin{align*}
    c   & = (X_1 + Z_1)^2 - (X_1 - Z_1)^2                   \\[-0.5ex]
    X_3 & = (X_1 + Z_1)^2(X_1-Z_1)^2                        \\[-0.5ex]
    Z_3 & = c\Big((X_1 + Z_1)^2+\frac{a-2}{4}\times c\Big),
  \end{align*}
  then for any point $P_1$ in $M_{a,b}(\K)$ such that $X_1/Z_1 = \chi(P_1)$,
  we have $X_3/Z_3 = \chi(2P_1)$.
\end{lemma}

With \lref{lemma:xADD} and \lref{lemma:xDBL}, we are able to compute efficiently
differential additions and point doublings using projective coordinates.

\subsubsection{Scalar multiplication algorithms}
\label{subsec:ECC-ladder}

By taking \aref{alg:montgomery-ladder} and replacing \texttt{xDBL\&ADD} by a
combination of the formulae from \lref{lemma:xADD} and \lref{lemma:xDBL},
we define a ladder \coqe{opt_montgomery} (in which $\K$ has not been fixed yet).
% similar to the one used in TweetNaCl (with \coqe{montgomery_rec}).
% shown above.

% We prove its correctness for any point whose \xcoord is not 0.
%
% \begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
% Lemma opt_montgomery_x :
%   forall (n m : nat) (x : K),
%   n < 2^m -> x != 0 ->
%   forall (p : mc M), p#x0 = x ->
%   opt_montgomery n m x = (p *+ n)#x0.
% \end{lstlisting}
% We can remark that for an input $x = 0$, the ladder returns $0$.
% \begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
% Lemma opt_montgomery_0:
%   forall (n m : nat), opt_montgomery n m 0 = 0.
% \end{lstlisting}
% Also \Oinf\ is the neutral element of $M_{a,b}(\K)$.
% \begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
% Lemma p_x0_0_eq_0 : forall (n : nat) (p : mc M),
%   p #x0 = 0%:R -> (p *+ n) #x0 = 0%R.
% \end{lstlisting}
% This gives us the theorem of the correctness of the Montgomery ladder.

This gives us the theorem of the correctness of the Montgomery ladder.
\begin{theorem}
  \label{thm:montgomery-ladder-correct}
  For all $n, m \in \N$, $x \in \K$, $P \in M_{a,b}(\K)$,
  if $\chi_0(P) = x$ then \coqe{opt_montgomery} returns $\chi_0(n \cdot P)$
\end{theorem}
\begin{lstlisting}[language=Coq]
Theorem opt_montgomery_ok (n m: nat) (x : K) :
  n < 2^m ->
  forall (p : mc M), p#x0 = x ->
  opt_montgomery n m x = (p *+ n)#x0.
\end{lstlisting}
The definition of \coqe{opt_montgomery} is similar to \coqe{montgomery_rec_swap}
that was used in \coqe{RFC}.
We proved their equivalence, and used it in our
final proof of \coqe{Theorem RFC_Correct}.


\subsection{Curves, twists and extension fields}
\label{subsec:curve_twist_fields}

\fref{tikz:ProofHighLevel2} gives a high-level view of the proofs presented here.
The white tiles are definitions while green tiles are important lemmas and theorems.

\begin{figure}[h]
  \centering
  \include{tikz/highlevel2}
  \vspace{-0.5cm}
  \caption{Proof dependencies for the correctness of X25519.}
  \label{tikz:ProofHighLevel2}
\end{figure}

A brief overview of the complete proof is described below.
We first pose $a = 486662$, $b = 1$, $b' = 2$, $p = 2^{255}-19$, with the equations $C = M_{a,b}$, and $T = M_{a,b'}$.
We prove the primality of $p$ and define the field $\F{p}$.
Subsequently, we show that neither $2$ nor $a^2 - 2$ are square in $\F{p}$.
We consider $\F{p^2}$ and define $C(\F{p})$, $T(\F{p})$, and $C(\F{p^2})$.
We prove that for all $x \in \F{p}$ there exists a point of \xcoord $x$ either on $C(\F{p})$ or on the quadratic twist $T(\F{p})$.
We prove that all points in $M(\F{p})$ and $T(\F{p})$ can be projected in $M(\F{p^2})$ and derive that computations done in $M(\F{p})$ and $T(\F{p})$ yield to the same results if projected to $M(\F{p^2})$.
Using \tref{thm:montgomery-ladder-correct} we prove that the ladder is correct for $M(\F{p})$ and $T(\F{p})$; with the previous results, this results in the correctness of the ladder for $M(\F{p^2})$, in other words the correctness of X25519.

Now that we have an red line for the proof, we turn our attention to the details.
Indeed \tref{thm:montgomery-ladder-correct} cannot be applied directly to prove that X25519 is
doing the computations over $M(\F{p^2})$. This would infer that $\K = \F{p^2}$ and we would need to satisfy
hypothesis~\ref{hyp:a_minus_4_not_square}:%
% $a^2-4$ is not a square in \K:
$$\forall x \in \K,\ x^2 \neq a^2-4.$$
which is not possible as there always exists $x \in \F{p^2}$ such that $x^2 = a^2-4$.
Consequently, we first study Curve25519 and one of its quadratic twists Twist25519,
both defined over \F{p}.

\subsubsection{Curves and twists}
\label{subsec:Zmodp}

We define $\F{p}$ as the numbers between $0$ and $p = \p$.
We create a \coqe{Zmodp} module to encapsulate those definitions.
\begin{lstlisting}[language=Coq]
Module Zmodp.
Definition betweenb x y z := (x <=? z) && (z <? y).
Definition p := locked (2^255 - 19).
Fact Hp_gt0 : p > 0.
Inductive type := Zmodp x of betweenb 0 p x.
\end{lstlisting}

We define the basic operations ($+, -, \times$) with their respective neutral
elements ($0, 1$) and prove \lref{lemma:Zmodp_field}.
\begin{lemma}
  \label{lemma:Zmodp_field}
  $\F{p}$ is a field.
\end{lemma}
For $a = 486662$, by using the Legendre symbol we prove that
$a^2 - 4$ and $2$ are not squares in $\F{p}$.
\begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
Fact a_not_square : forall x: Zmodp.type,
  x^+2 != (Zmodp.pi 486662)^+2 - 4%:R.
\end{lstlisting}
\begin{lstlisting}[language=Coq,label=two_not_square,belowskip=-0.1 \baselineskip]
Fact two_not_square : forall x: Zmodp.type,
  x^+2 != 2%:R.
\end{lstlisting}
We now consider $M_{486662,1}(\F{p})$ and $M_{486662,2}(\F{p})$, one of its quadratic twists.
% \begin{dfn}Let the following instantiations of \aref{alg:montgomery-double-add}:\\
\begin{dfn}
  %Let the following instantiations of \aref{alg:montgomery-ladder}:\\
  We instantiate \coqe{opt_montgomery} in two specific ways:
  \begin{itemize}
    \item[--] $Curve25519\_Fp(n,x)$ for $M_{486662,1}(\F{p})$.
    \item[--] $Twist25519\_Fp(n,x)$ for $M_{486662,2}(\F{p})$.
  \end{itemize}
\end{dfn}

With \tref{thm:montgomery-ladder-correct} we derive the following two lemmas:
\begin{lemma}
  For all $x \in \F{p},\ n \in \N,\ P \in \F{p} \times \F{p}$,\\
  such that $P \in M_{486662,1}(\F{p})$ and $\chi_0(P) = x$.
  $$Curve25519\_Fp(n,x) = \chi_0(n \cdot P)$$
\end{lemma}
\begin{lemma}
  For all $x \in \F{p},\ n \in \N,\ P \in \F{p} \times \F{p}$\\
  such that $P \in M_{486662,2}(\F{p})$ and $\chi_0(P) = x$.
  $$Twist25519\_Fp(n,x) = \chi_0(n \cdot P)$$
\end{lemma}
As the Montgomery ladder does not depend on $b$, it is trivial to
see that the computations done for points in $M_{486662,1}(\F{p})$ and in
$M_{486662,2}(\F{p})$ are the same.
\begin{lstlisting}[language=Coq]
Theorem curve_twist_eq: forall n x,
  curve25519_Fp_ladder n x = twist25519_Fp_ladder n x.
\end{lstlisting}

Because $2$ is not a square in $\F{p}$, it allows us split $\F{p}$ into two sets.
\begin{lemma}
  \label{lemma:square-or-2square}
  For all $x$ in $\F{p}$, there exists $y$ in $\F{p}$ such that
  $$y^2 = x\ \ \ \lor\ \ 2y^2 = x$$
\end{lemma}
For all $x \in \F{p}$, we can compute $x^3 + ax^2 + x$. Using \lref{lemma:square-or-2square}
we can find a $y$ such that $(x,y)$ is either on the curve or on the quadratic twist:
\begin{lemma}
  \label{lemma:curve-or-twist}
  For all $x \in \F{p}$, there exists a point $P$ in $M_{486662,1}(\F{p})$ or
  in $M_{486662,2}(\F{p})$ such that the \xcoord of $P$ is $x$.
\end{lemma}
\begin{lstlisting}[language=Coq,belowskip=-0.5 \baselineskip]
Theorem x_is_on_curve_or_twist:
  forall x : Zmodp.type,
  (exists (p : mc curve25519_mcuType), p#x0 = x) \/
  (exists (p' : mc twist25519_mcuType), p'#x0 = x).
\end{lstlisting}

\subsubsection{Curve25519 over \F{p^2}}
\label{subsec:curvep2}

The quadratic extension $\F{p^2}$ is defined as $\F{p}[\sqrt{2}]$ by~\cite{Ber06}.
The theory of finite fields already has been formalized in the Mathematical Components
library,
%ref?
but this formalization is rather abstract, and we need concrete representations of field
elements here.
For this reason we decided to formalize a definition of $\F{p^2}$ ourselves.

We can represent $\F{p^2}$ as the set $\F{p} \times \F{p}$,
% in other words,
representing polynomials with coefficients in $\F{p}$ modulo $X^2 - 2$. In a similar way
as for $\F{p}$ we use a module in Coq.
\begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
Module Zmodp2.
Inductive type :=
  Zmodp2 (x: Zmodp.type) (y:Zmodp.type).

Definition pi (x: Zmodp.type * Zmodp.type) : type :=
  Zmodp2 x.1 x.2.
Definition mul (x y: type) : type :=
  pi ((x.1 * y.1) + (2%:R * (x.2 * y.2)),
      (x.1 * y.2) + (x.2 * y.1)).
\end{lstlisting}
% Definition zero : type :=
%   pi ( 0%:R, 0%:R ).
% Definition one : type :=
%   pi ( 1, 0%:R ).
% Definition opp (x: type) : type :=
%   pi (- x.1 , - x.2).
% Definition add (x y: type) : type :=
%   pi (x.1 + y.1, x.2 + y.2).
% Definition sub (x y: type) : type :=
%   pi (x.1 - y.1, x.2 - y.2).

We define the basic operations ($+, -, \times$) with their respective neutral
elements $0$ and $1$. Additionally we verify that for each element of in
$\F{p^2}\backslash\{0\}$, there exists a multiplicative inverse.
\begin{lemma}
  \label{lemma:Zmodp2_inv}
  For all $x \in \F{p^2}\backslash\{0\}$ and $a,b \in \F{p}$ such that $x = (a,b)$,
  $$x^{-1} = \Big(\frac{a}{a^2-2b^2}\ , \frac{-b}{a^2-2b^2}\Big)$$
\end{lemma}
As in $\F{p}$, we define $0^{-1} = 0$ and prove \lref{lemma:Zmodp2_field}.
\begin{lemma}
  \label{lemma:Zmodp2_field}
  $\F{p^2}$ is a commutative field.
\end{lemma}

%% TOO LONG
%% If need remove this paragraph
We then specialize the basic operations in order to speed up the verification
of formulas by using rewrite rules:
\begin{equation*}
  \begin{split}
    (a,0) + (b,0) &= (a+b, 0)\\[-0.5ex]
    (a, 0)^{-1} &= (a^{-1}, 0)
  \end{split}
  \qquad
  \begin{split}
    (a,0) \cdot   (b,0) &= (a \cdot b, 0)\\[-0.5ex]
    (0,a)^{-1} &= (0,(2\cdot a)^{-1})
  \end{split}
\end{equation*}

The injection $a \mapsto (a,0)$ from $\F{p}$ to $\F{p^2}$ preserves
$0, 1, +, -, \times$. Thus $(a,0)$ can be abbreviated as $a$ without confusion.

We define $M_{486662,1}(\F{p^2})$. With the rewrite rule above, it is straightforward
to prove that any point on the curve $M_{486662,1}(\F{p})$ is also on the curve
$M_{486662,1}(\F{p^2})$. Similarly, any point on the quadratic twist
$M_{486662,2}(\F{p})$ also corresponds to a point on the curve $M_{486662,1}(\F{p^2})$.
As direct consequence, using \lref{lemma:curve-or-twist}, we prove that for all
$x \in \F{p}$, there exists a point $P \in \F{p^2}\times\F{p^2}$ on
$M_{486662,1}(\F{p^2})$ such that $\chi_0(P) = (x,0) = x$.

\begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
Lemma x_is_on_curve_or_twist_implies_x_in_Fp2:
  forall (x:Zmodp.type),
    exists (p: mc curve25519_Fp2_mcuType),
      p#x0 = Zmodp2.Zmodp2 x 0.
\end{lstlisting}

We now study the case of the scalar multiplication and show similar proofs.
\begin{dfn}
  Define the functions $\varphi_c$, $\varphi_t$ and $\psi$
  \begin{itemize}
    \item[--] $\varphi_c: M_{486662,1}(\F{p}) \mapsto M_{486662,1}(\F{p^2})$\\
          such that $\varphi((x,y)) = ((x,0), (y,0))$.
    \item[--] $\varphi_t: M_{486662,2}(\F{p}) \mapsto M_{486662,1}(\F{p^2})$\\
          such that $\varphi((x,y)) = ((x,0), (0,y))$.
    \item[--] $\psi: \F{p^2} \mapsto \F{p}$ such that $\psi(x,y) = x$.
  \end{itemize}
\end{dfn}

\begin{lemma}
  \label{lemma:proj}
  For all $n \in \N$, for all point $P\in\F{p}\times\F{p}$ on the curve
  $M_{486662,1}(\F{p})$ (respectively on the quadratic twist $M_{486662,2}(\F{p})$), we have
  \vspace{-0.3em}
  \begin{align*}
    P & \in M_{486662,1}(\F{p}) & \implies \varphi_c(n \cdot P) & = n \cdot \varphi_c(P), &  & \text{and} \\[-0.5ex]
    P & \in M_{486662,2}(\F{p}) & \implies \varphi_t(n \cdot P) & = n \cdot \varphi_t(P).
  \end{align*}
\end{lemma}
Notice that
\vspace{-0.5em}
\begin{align*}
  \forall P \in M_{486662,1}(\F{p}), &  & \psi(\chi_0(\varphi_c(P))) & = \chi_0(P), &  & \text{and} \\[-0.5ex]
  \forall P \in M_{486662,2}(\F{p}), &  & \psi(\chi_0(\varphi_t(P))) & = \chi_0(P).
\end{align*}

In summary, for all $n \in \N$, $n < 2^{255}$, for any point $P\in\F{p}\times\F{p}$
in $M_{486662,1}(\F{p})$ or $M_{486662,2}(\F{p})$, $Curve25519\_Fp$
computes $\chi_0(n \cdot P)$.
We have proved that for all $P \in \F{p^2}\times\F{p^2}$ such that $\chi_0(P) \in \F{p}$,
there exists a corresponding point on the curve or the twist over $\F{p}$.
Moreover, we have proved that for any point on the curve or the twist, we can compute the
scalar multiplication by $n$ and obtain the same result as if we did the
computation in $\F{p^2}$.
% As a result we have proved theorem 2.1 of \cite{Ber06}:
% No: missing uniqueness !
\begin{theorem}
  \label{thm:general-scalarmult}
  For all $n \in \N$, such that $n < 2^{255}$,
  for all $x \in \F{p}$ and $P \in M_{486662,1}(\F{p^2})$ such that $\chi_0(P) = x$,
  $Curve25519\_Fp(n,x)$ computes $\chi_0(n \cdot P)$.
\end{theorem}
% which is formalized in Coq as:
% \begin{lstlisting}[language=Coq,belowskip=-0.1 \baselineskip]
% Theorem curve25519_Fp2_ladder_ok:
%   forall (n : nat) (x:Zmodp.type),
%   (n < 2^255)%nat ->
%   forall (p  : mc curve25519_Fp2_mcuType),
%   p #x0 = Zmodp2.Zmodp2 x 0 ->
%   curve25519_Fp_ladder n x = (p *+ n)#x0 /p.
% \end{lstlisting}

We then prove the equivalence of operations between $\Ffield$ and $\Zfield$,
in other words between \coqe{Zmodp} and \coqe{:GF}.
This allows us to show that given a clamped value $n$ and normalized \xcoord of $P$,
\coqe{RFC} gives the same results as $Curve25519\_Fp$.

All put together, this finishes the proof of the mathematical correctness of X25519: the fact that the code in X25519, both in the RFC~7748 and
in TweetNaCl versions, correctly computes multiplication in the elliptic curve.