Commit fc994792 authored by benoit's avatar benoit
Browse files

more trim

parent 3fda7747
...@@ -4,6 +4,7 @@ ...@@ -4,6 +4,7 @@
\subheading{Verified C Code} We provide below the code we verified. \subheading{Verified C Code} We provide below the code we verified.
\lstinputlisting[linerange={2-5,8-9,266-317,333-380,393-438},language=Ctweetnacl]{../proofs/vst/c/tweetnaclVerifiableC.c} \lstinputlisting[linerange={2-5,8-9,266-317,333-380,393-438},language=Ctweetnacl]{../proofs/vst/c/tweetnaclVerifiableC.c}
~
\subheading{Diff from TweetNaCl} We provide below the diff between the original code of TweetNaCl and the code we verified. \subheading{Diff from TweetNaCl} We provide below the diff between the original code of TweetNaCl and the code we verified.
......
...@@ -92,8 +92,7 @@ Inductive point := EC_Inf | EC_In of K * K. ...@@ -92,8 +92,7 @@ Inductive point := EC_Inf | EC_In of K * K.
Notation "(| x, y |)" := (EC_In x y). Notation "(| x, y |)" := (EC_In x y).
Notation "\infty" := (EC_Inf). Notation "\infty" := (EC_Inf).
Record ecuType := Record ecuType := { A : K; B : K; _: 4 * A^3 + 27 * B^2 != 0}.
{ A : K; B : K; _ : 4 * A^3 + 27 * B^2 != 0}.
Definition oncurve (p : point) := Definition oncurve (p : point) :=
if p is (| x, y |) if p is (| x, y |)
then y^2 == x^3 + A * x + B then y^2 == x^3 + A * x + B
...@@ -152,8 +151,7 @@ a \texttt{K : ecuFieldType} ---the type of fields whose characteristic is neithe ...@@ -152,8 +151,7 @@ a \texttt{K : ecuFieldType} ---the type of fields whose characteristic is neithe
2 nor 3--- and \texttt{M : mcuType} ---a record that packs the curve 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$. 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] \begin{lstlisting}[language=Coq,belowskip=-0.1 \baselineskip]
Record mcuType := Record mcuType := { cA : K; cB : K; _: cB != 0; _: cA^2 != 4}.
{ cA : K; cB : K; _ : cB != 0; _ : cA^2 != 4}.
Definition oncurve (p : point K) := Definition oncurve (p : point K) :=
if p is (| x, y |) if p is (| x, y |)
then cB * y^+2 == x^+3 + cA * x^+2 + x then cB * y^+2 == x^+3 + cA * x^+2 + x
...@@ -249,8 +247,7 @@ we ensure that $(0,0)$ is the only point with a $y$-coordinate of $0$. ...@@ -249,8 +247,7 @@ we ensure that $(0,0)$ is the only point with a $y$-coordinate of $0$.
The number $a^2-4$ is not a square in \K. The number $a^2-4$ is not a square in \K.
\end{hypothesis} \end{hypothesis}
\begin{lstlisting}[language=Coq] \begin{lstlisting}[language=Coq]
Hypothesis mcu_no_square : Hypothesis mcu_no_square : forall x : K, x^+2 != (M#a)^+2 - 4%:R.
forall x : K, x^+2 != (M#a)^+2 - 4%:R.
\end{lstlisting} \end{lstlisting}
We define $\chi$ and $\chi_0$ to return the \xcoord of points on a curve. We define $\chi$ and $\chi_0$ to return the \xcoord of points on a curve.
...@@ -401,15 +398,15 @@ elements ($0, 1$) and prove \lref{lemma:Zmodp_field}. ...@@ -401,15 +398,15 @@ elements ($0, 1$) and prove \lref{lemma:Zmodp_field}.
\end{lemma} \end{lemma}
For $a = 486662$, by using the Legendre symbol we prove that For $a = 486662$, by using the Legendre symbol we prove that
$a^2 - 4$ and $2$ are not squares in $\F{p}$. $a^2 - 4$ and $2$ are not squares in $\F{p}$.
\begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip] % \begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
Fact a_not_square : forall x: Zmodp.type, % Fact a_not_square : forall x: Zmodp.type,
x^+2 != (Zmodp.pi 486662)^+2 - 4%:R. % x^+2 != (Zmodp.pi 486662)^+2 - 4%:R.
\end{lstlisting} % \end{lstlisting}
\begin{lstlisting}[language=Coq,label=two_not_square,belowskip=-0.1 \baselineskip] % \begin{lstlisting}[language=Coq,label=two_not_square,belowskip=-0.1 \baselineskip]
Fact two_not_square : forall x: Zmodp.type, % Fact two_not_square : forall x: Zmodp.type,
x^+2 != 2%:R. % x^+2 != 2%:R.
\end{lstlisting} % \end{lstlisting}
We now consider $M_{486662,1}(\F{p})$ and $M_{486662,2}(\F{p})$, one of its quadratic twists. This allows us to study $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-double-add}:\\
\begin{dfn} \begin{dfn}
%Let the following instantiations of \aref{alg:montgomery-ladder}:\\ %Let the following instantiations of \aref{alg:montgomery-ladder}:\\
...@@ -434,10 +431,10 @@ With \tref{thm:montgomery-ladder-correct} we derive the following two lemmas: ...@@ -434,10 +431,10 @@ With \tref{thm:montgomery-ladder-correct} we derive the following two lemmas:
As the Montgomery ladder does not depend on $b$, it is trivial to 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 see that the computations done for points in $M_{486662,1}(\F{p})$ and in
$M_{486662,2}(\F{p})$ are the same. $M_{486662,2}(\F{p})$ are the same.
\begin{lstlisting}[language=Coq] % \begin{lstlisting}[language=Coq]
Theorem curve_twist_eq: forall n x, % Theorem curve_twist_eq: forall n x,
curve25519_Fp_ladder n x = twist25519_Fp_ladder n x. % curve25519_Fp_ladder n x = twist25519_Fp_ladder n x.
\end{lstlisting} % \end{lstlisting}
Because $2$ is not a square in $\F{p}$, it allows us split $\F{p}$ into two sets. Because $2$ is not a square in $\F{p}$, it allows us split $\F{p}$ into two sets.
\begin{lemma} \begin{lemma}
......
...@@ -112,38 +112,38 @@ We define the little-endian projection to integers as follows. ...@@ -112,38 +112,38 @@ We define the little-endian projection to integers as follows.
Let \Coqe{ZofList} : $\Z \rightarrow \texttt{list}~\Z \rightarrow \Z$, Let \Coqe{ZofList} : $\Z \rightarrow \texttt{list}~\Z \rightarrow \Z$,
a function given $n$ and a list $l$ returns its little endian decoding with radix $2^n$. a function given $n$ and a list $l$ returns its little endian decoding with radix $2^n$.
\end{dfn} \end{dfn}
\begin{lstlisting}[language=Coq,aboveskip=0pt,belowskip=1pt] % \begin{lstlisting}[language=Coq,aboveskip=0pt,belowskip=1pt]
Fixpoint ZofList {n:Z} (a:list Z) : Z := % Fixpoint ZofList {n:Z} (a:list Z) : Z :=
match a with % match a with
| [] => 0 % | [] => 0
| h :: q => h + 2^n * ZofList q % | h :: q => h + 2^n * ZofList q
end. % end.
\end{lstlisting} % \end{lstlisting}
The encoding from integers to bytes is defined in a similar way. Similarly, we define the encoding from integers to bytes.
\begin{dfn} \begin{dfn}
Let \Coqe{ListofZ32} : $\Z \rightarrow \Z \rightarrow \texttt{list}~\Z$, given Let \Coqe{ListofZ32} : $\Z \rightarrow \Z \rightarrow \texttt{list}~\Z$, given
$n$ and $a$ returns $a$'s little-endian encoding as a list with radix $2^n$. $n$ and $a$ returns $a$'s little-endian encoding as a list with radix $2^n$.
%XXX-Peter: Again I'm confused... why are there two \rightarrows? %XXX-Peter: Again I'm confused... why are there two \rightarrows?
%XXX-Benoit it is the functional view of arguments and partial functions. It is called Currying. %XXX-Benoit it is the functional view of arguments and partial functions. It is called Currying.
\end{dfn} \end{dfn}
\begin{lstlisting}[language=Coq,aboveskip=1pt,belowskip=1pt] % \begin{lstlisting}[language=Coq,aboveskip=1pt,belowskip=1pt]
Fixpoint ListofZn_fp {n:Z} (a:Z) (f:nat) : list Z := % Fixpoint ListofZn_fp {n:Z} (a:Z) (f:nat) : list Z :=
match f with % match f with
| 0%nat => [] % | 0%nat => []
| S fuel => (a mod 2^n) :: ListofZn_fp (a/2^n) fuel % | S fuel => (a mod 2^n) :: ListofZn_fp (a/2^n) fuel
end. % end.
Definition ListofZ32 {n:Z} (a:Z) : list Z := % Definition ListofZ32 {n:Z} (a:Z) : list Z :=
ListofZn_fp n a 32. % ListofZn_fp n a 32.
\end{lstlisting} % \end{lstlisting}
In order to increase the trust in our formalization, we prove that % In order to increase the trust in our formalization, we prove that
\Coqe{ListofZ32} and \Coqe{ZofList} are inverse to each other. % \Coqe{ListofZ32} and \Coqe{ZofList} are inverse to each other.
\begin{lstlisting}[language=Coq,aboveskip=1pt,belowskip=1pt] % \begin{lstlisting}[language=Coq,aboveskip=1pt,belowskip=1pt]
Lemma ListofZ32_ZofList_Zlength: forall (l:list Z), % Lemma ListofZ32_ZofList_Zlength: forall (l:list Z),
Forall (fun x => 0 <= x < 2^n) l -> % Forall (fun x => 0 <= x < 2^n) l ->
Zlength l = 32 -> % Zlength l = 32 ->
ListofZ32 n (ZofList n l) = l. % ListofZ32 n (ZofList n l) = l.
\end{lstlisting} % \end{lstlisting}
With those tools at hand, we formally define the decoding and encoding as With those tools at hand, we formally define the decoding and encoding as
specified in the RFC. specified in the RFC.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment