Commit d55757a2 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

put the actual theorem in the paper

parent 4759a1ab
......@@ -271,17 +271,18 @@ As Post-condition we have:
We show that the computation for \VSTe{CSM} fits in \TNaCle{u8[32]}.
\end{itemize}
\todo[inline]{theorem between CSM and Timmy representation here. Eg.}
\begin{lstlisting}[language=Coq]
Theorem CSM_eq :
forall (n:list Z) (p:list Z),
Zlength n = 16 ->
Zlength p = 16 ->
Forall (fun x => 0 <= x < 2^8) p ->
Forall (fun x => 0 <= x < 2^8) n ->
Z16.lst (CSM n p) = Z16.lst n $\times$ Z16.lst p.
Theorem Crypto_Scalarmult_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 (ZUnpack25519 (ZofList 8 p)) = P#x0 ->
ZofList 8 (Crypto_Scalarmult n p) =
(P *+ (Z.to_nat (Zclamp (ZofList 8 n)))) _x0.
\end{lstlisting}
We proved that \VSTe{crypto_scalarmult} (\VSTe{CSM} in Coq)
computes: $$Q.x \leftarrow N \times P.x$$
......
......@@ -35,7 +35,7 @@
% Usenix wants no page numbers for camera-ready papers, so that they can
% number them themselves. But submitted papers should have page numbers
% for the reviewers' convenience.
%
%
%
% \pagestyle{empty}
......
Supports Markdown
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