Some more intro text.

paper/1-intro.tex

@@ -80,12 +80,22 @@ matches the specification.
 \todo{Say something about all X25519 implementations from the SoK paper.}
 The work described in~\cite{XXX}
 
+The X25519 implementation from the Everycrypt project~\cite{}
+uses a low-level language called Vale that translates
+directly to assembly and proves equivalence to a high-level specification in F$^*$.
+evercrypt
+hacl*
+jasmin
+fiat
+
+
+
 
 %The synthesis approach was used by Zinzindohou{\'{e}}, Bartzia, and Bhargavan to build a verified extensible
 %library of elliptic curves~\cite{Zinzindohoue2016AVE} in F*~\cite{DBLP:journals/corr/BhargavanDFHPRR17}.
 %This served as ground work for the cryptographic library HACL*~\cite{zinzindohoue2017hacl}
 %used in the NSS suite from Mozilla.
-%
+
 %Coq not only allows verification but also synthesis~\cite{CpdtJFR}.
 %Erbsen, Philipoom, Gross, and Chlipala make use of it to have
 %correct-by-construction finite field arithmetic, which is used
@@ -93,10 +103,8 @@ The work described in~\cite{XXX}
 %This software suite is now being used in BoringSSL~\cite{fiat-crypto}.
 
 
-All of these X25519 verification efforts listed in~\cite{BBB+19} use a clean-slate
-approach to obtain code and proofs.
-Our effort targets existing software and we are aware of only one earlier
-work in the context of X25519 following a similar approach.
+All of these X25519 verification efforts use a clean-slate approach to obtain code and proofs.
+Our effort targets existing software; we are aware of only one earlier work verifying existing X25519 software.
 In~\cite{Chen2014VerifyingCS}, Chen, Hsu, Lin, Schwabe, Tsai, Wang, Yang, and Yang present
 a mechanized proof of two assembly-level implementations of the core function of X25519.
 The proof in~\cite{Chen2014VerifyingCS} takes a different approach from ours.