\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.
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}
  \caption{Overview of the proof of Montgomery ladder's correctness}
  \label{tikz:ProofHighLevel1}
\end{figure}

\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 commutative 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, Q \in E_{a,b}(\K) \setminus \{\Oinf\}$ with $P \neq Q$ and $P \neq -Q$
      is defined as the negation of the third intersection point of the line through $P$ and $Q$.
      In case $P = Q$, we either use the line tangent to $P$ if $P$ is not an inflection point,
        and define $P + Q = -P = -Q$ otherwise.
      In case $P = -Q$, we define $P + Q = \Oinf$.
  \item The point $\Oinf$ acts as the neutral element. Hence, we define $-\Oinf = \Oinf$,
      $P + \Oinf = P$ and $\Oinf + P = P$.
\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: % (again with coercion):
\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}

Remarkably, of all the group properties, associativity is the hardest one to prove for elliptic curves.
Instead of reproving this property for Montgomery curves, we transfer it from the Weierstra{\ss} curves
with a trick.
We define a bijection between a Montgomery curve and its short Weierstra{\ss} form
(as in \lref{lemma:bij-ecc})
and prove that it respects the addition as defined on the respective curves.
It is then easy to verify all the group laws for Montgomery curves from the Weierstra{\ss} ones.

After we have 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
  $$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} \to E_{a',b'}$ defined as:
  \begin{align*}
    \varphi(\Oinf_M)   & = \Oinf_E                                                 \\
    \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 eachother, \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) \to \K \cup \{\infty\}$ and $\chi_0 : M_{a,b}(\K) \to \K$ such that
    \begin{align*}
        \chi((x,y)) &= x, & \chi(\Oinf) &= \infty, &&\text{and} \\
        \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
  \begin{align*}
    X_3 & = Z_4((X_1 - Z_1)(X_2+Z_2) + (X_1+Z_1)(X_2-Z_2))^2  \\
    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                   \\
    X_3 & = (X_1 + Z_1)^2(X_1-Z_1)^2                        \\
    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}
  \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 exist 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)\\
    (a, 0)^{-1} &= (a^{-1}, 0)
  \end{split}
  \qquad
  \begin{split}
    (a,0) \cdot   (b,0) &= (a \cdot b, 0)\\
    (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
  \begin{align*}
      P &\in M_{486662,1}(\F{p}) & \implies \varphi_c(n \cdot P) &= n \cdot \varphi_c(P), &&\text{and} \\
      P &\in M_{486662,2}(\F{p}) & \implies \varphi_t(n \cdot P) &= n \cdot \varphi_t(P).
  \end{align*}
\end{lemma}
Notice that
\begin{align*}
    \forall P \in M_{486662,1}(\F{p}), &&\psi(\chi_0(\varphi_c(P))) &= \chi_0(P), &&\text{and} \\
    \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.